Definition transport_type_path {X Y:Type} (p:X = Y) (x:X) : transportf (λ T:Type, T) p x = cast p x. Proof. reflexivity. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics.