proposition: Theorem pequiv_pclassifyingspace_pi1 `{Univalence} (X : pType) `{IsConnected 0 X} `{IsTrunc 1 X} : B (Pi1 X) <~>* X.
proof: Proof. transparent assert (f : (B (Pi1 X) ->* X)). { snrapply pClassifyingSpace_rec. 1: exact _. 1: exact (equiv_tr 0 _)^-1%equiv. intros x y. strip_truncations. reflexivity. } snrapply (Build_pEquiv _ _ f). apply isequiv_is0connected_isequiv_loops. snrapply (cancelR_isequiv bloop). 1: exact _. rapply isequiv_homotopic'; symmetry. nrapply pClassifyingSpace_rec_beta_bloop. Defined.
imports: Basics Types Pointed Cubical WildCat Algebra.AbGroups Homotopy.HSpace.Core TruncType Truncations.Core Truncations.Connectedness Homotopy.HomotopyGroup Homotopy.WhiteheadsPrinciple