`{Funext} {A} : IsHProp A <~> (A -> Contr A). Proof. apply (equiv_adjointify (@contr_inhabited_hprop A) (@hprop_inhabited_contr A)). - intro ic. by_extensionality x. apply @path_contr. apply contr_istrunc. exact (ic x). - intro hp. apply path_ishprop. Defined.
Require Import HoTT.Basics HoTT.Types.