fact: Definition equiv_functor_arrow' `(f : B <~> A) `(g : C <~> D) : (A -> C) <~> (B -> D) := @equiv_functor_forall' _ A (fun _ => C) B (fun _ => D) f (fun _ => g).
imports: Basics.Overture Basics.PathGroupoids Basics.Decidable Basics.Equivalences Basics.Trunc Basics.Tactics Types.Forall