Definition PathOverConstant_map2_eq2 {X:Type} {x x':X} (p:x=x') {Z : Type} {z z' z'' : Z} (r : z = z') (q: PathOver p z' z'') : PathOverConstant_map2 (r ⟤ q) = r @ PathOverConstant_map2 q. Proof. now induction r. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.