Definition composePathOver {X:Type} {x x' x'':X} {p:x=x'} {p':x'=x''} {Y : X -> Type} {y : Y x} {y' : Y x'} {y'' : Y x''} : PathOver p y y' → PathOver p' y' y'' → PathOver (p @ p') y y''. Proof. induction p, p'. exact pathscomp0. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.