Definition transportf_weq_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' := make_weq _ (isweq_transportf_to_pathover p y y').
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.