Definition composePathOverLeftInverse {X:Type} {x x':X} {Y : X -> Type} {y : Y x} {y' : Y x'} {p:x=x'} (q : PathOver p y y') : q^-1 * q = cp (!pathsinv0l p) (identityPathOver y'). Proof. now induction p, q. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.