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. now induction q. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.