`{Funext} {A} : Contr A <~> A * forall (x y : A), x = y. Proof. transitivity (A * IsHProp A). - apply equiv_contr_inhabited_hprop. - exact (1 *E equiv_hprop_allpath _). Defined.
Require Import HoTT.Basics HoTT.Types.