Lemma transport_functions {X} {Y:X->Type} {Z:∏ x (y:Y x), Type} {f f':∏ x : X, Y x} (p:f = f') (z:∏ x, Z x (f x)) x : transportf (λ f, ∏ x, Z x (f x)) p z x = transportf (Z x) (toforallpaths _ _ _ p x) (z x). Proof. intros. induction p. reflexivity. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics.