(A B : Type) `{Contr A} : (A -> B) <~> B. Proof. srapply (equiv_adjointify (fun f => f (center A)) const). - reflexivity. - intro f; funext a; unfold const; simpl. apply (ap f), contr. Defined.
Require Import Basics.Overture Basics.PathGroupoids Basics.Decidable Require Import Types.Forall.