Definition inversePathOverIdpath' {X:Type} {x:X} {Y : X -> Type} (y y' : Y x) (e : y = y') : inversePathOver' (∇ e : PathOver (! idpath x) y y') = ∇ (!e). Proof. reflexivity. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.