Definition transport_invmap {T} {X Y:T->Type} (f:∏ t, (X t) ≃ (Y t)) {t t':T} (p:t=t') : transportf (λ t, Y t -> X t) p (invmap (f t)) = invmap (transportf (λ t, (X t) ≃ (Y t)) p (f t)). Proof. intros. induction p. reflexivity. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics.