Definition inversePathOver {X:Type} {x x':X} {p:x=x'} {Y : X -> Type} {y : Y x} {y' : Y x'} : PathOver p y y' → PathOver (!p) y' y. Proof. intros q. induction p, q. reflexivity. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.