Definition PathOverToTotalPath {X:Type} {x x':X} (p:x=x') {Y : X -> Type} (y : Y x) (y' : Y x') : PathOver p y y' → (x,,y) = (x',,y'). Proof. intros q. exact (invmap (total2_paths_equiv Y (x,, y) (x',, y')) (PathOverToPathPair q)). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.