fact: Definition equiv_functor_arrow `{IsEquiv B A f} `{IsEquiv C D g} : (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