proposition: Theorem transport_arrow_toconst_path_universe {A U V : Type} (w : U <~> V) : forall f : U -> A, transport (fun E : Type => E -> A) (path_universe w) f = (f o w^-1).
proof: Proof. intros f. funext y. refine (transport_arrow_toconst _ _ _ @ _). apply ap. apply transport_path_universe_V. Defined.
imports: HoTT.Basics Types.Sigma Types.Forall Types.Arrow Types.Paths Types.Equiv Types.Bool Types.Prod