Definition transportPathTotal {X:Type} {x x':X} {Y : X -> Type} (y : Y x) (y' : Y x') (r : (x,,y) = (x',,y')) (T : ∏ (a:X) (b:Y a), Type) : T x y → T x' y'. Proof. induction (total2_paths_equiv _ _ _ r) as [p q]. change (x=x') in p. change (transportf _ p y = y') in q. induction p. change (y=y') in q. induction q. trivial. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics.