Definition PathOverConstant_map2 {X:Type} {x x':X} {p:x=x'} {Z : Type} {z z' : Z} : PathOver p z z' -> z = z'. Proof. now induction p. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.