RespectsEquivalenceR A (fun _ _ => Unit) := @const_respects_equivalenceR A Unit. End unit. Section prod. Global Instance prod_respects_equivalenceL {A} {P Q : forall B, (A <~> B) -> Type} `{RespectsEquivalenceL A P, RespectsEquivalenceL A Q} : RespectsEquivalenceL A (fun B e => P B e * Q B e). Proof. refine ((fun B e => equiv_functor_prod' (respects_equivalenceL.1 B e) (respects_equivalenceL.1 B e)); _). exact (fun fs => transport (fun e' => _ = equiv_functor_prod' e' _) (respects_equivalenceL.2 _) (transport (fun e' => _ = equiv_functor_prod' _ e') (respects_equivalenceL.2 _) idpath)). Defined.
Require Import Basics.Overture Basics.Equivalences Basics.Tactics. Require Import Types.Equiv Types.Prod Types.Forall Types.Sigma Types.Universe.