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