Lemma transport_idfun {X} (P:X->UU) {x y:X} (p:x = y) (u:P x) : transportf P p u = transportf (idfun UU) (maponpaths P p) u. Proof. intros. induction p. reflexivity. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics.