Definition inverseInversePathOver {X:Type} {Y : X -> Type} {x:X} {y : Y x} : ∏ {x':X} {y' : Y x'} {p:x=x'} (q : PathOver p y y'), transportf (λ pp, PathOver pp y y') (pathsinv0inv0 p) (q^-1^-1) = q. Proof. now use inductionPathOver. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.