RespectsEquivalenceL A (fun _ _ => Unit) := @const_respects_equivalenceL A Unit.
Require Import Basics.Overture Basics.Equivalences Basics.Tactics. Require Import Types.Equiv Types.Prod Types.Forall Types.Sigma Types.Universe.