Definition isweq_transportf_to_pathover {X : Type} {x x' : X} (p : x=x') {Y : X -> Type} (y : Y x) (y' : Y x') : isweq (transportf_to_pathover p y y'). Proof. use isweq_iso; intro; now induction p. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.