`{Funext} {A} : Contr A <~> A * IsHProp A. Proof. assert (f : Contr A -> A * IsHProp A). - intro P. split. + exact (@center _ P). + apply @istrunc_succ. exact P. - assert (g : A * IsHProp A -> Contr A). + intros [a P]. apply (@contr_inhabited_hprop _ P a). + refine (@equiv_iff_hprop _ _ _ _ f g). apply hprop_inhabited_contr; intro p. apply @contr_prod. * exact (g p). * apply (@contr_inhabited_hprop _ _ (snd p)). Defined.
Require Import HoTT.Basics HoTT.Types.