proposition: Lemma composePathPathOverPath {X:Type} {x x':X} {p:x=x'} {Y : X -> Type} {y y' : Y x} {y'' y''': Y x'} (q : y = y') (r : PathOver p y' y'') (s : y'' = y''') : q ⟤ (r ⟥ s) = (q ⟤ r) ⟥ s.
proof: Proof. now induction q. Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.PartA