Definition transportf_to_pathover {X:Type} {x x':X} (p:x=x') {Y : X -> Type} (y : Y x) (y' : Y x') : (transportf _ p y = y') → PathOver p y y'. Proof. intro. now induction p. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.