Definition PathOverConstant_map2_eq1 {X:Type} {x x':X} {p:x=x'} {Z : Type} {z z' z'' : Z} (q: PathOver p z z') (r : z' = z'') : PathOverConstant_map2 (q ⟥ r) = PathOverConstant_map2 q @ r. Proof. induction r. change (q ⟥ idpath z') with q. apply pathsinv0, pathscomp0rid. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.