`{IsEquiv B A f} `{IsEquiv C D g} : (A -> C) <~> (B -> D) := @equiv_functor_forall _ A (fun _ => C) B (fun _ => D) f _ (fun _ => g) _.
Require Import Basics.Overture Basics.PathGroupoids Basics.Decidable Require Import Types.Forall.