Definition transportf_pathsinv0 {X} (P:X->UU) {x y:X} (p:x = y) (u:P x) (v:P y) : transportf _ (!p) v = u -> transportf _ p u = v. Proof. intro e. induction p, e. reflexivity. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics.