Definition composePathOverPath_compute {X:Type} {x x':X} {p:x=x'} {Y : X -> Type} {y : Y x} {y' y'' : Y x'} (q : PathOver p y y') (e : y' = y'') : q ⟥ e = cp (pathscomp0rid p) (q * ∇ e). Proof. now induction p, q, e. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.