proposition: 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: Proof. intros. induction p. reflexivity. Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.Tactics