proposition: Theorem equiv_bg_pi1_adjoint `{Univalence} (X : pType) `{IsConnected 0 X} (G : Group) : (Pi 1 X $-> G) <~> (X $-> B G).
proof: Proof. rapply natequiv_bg_pi1_adjoint. Defined.
imports: Basics Types Pointed Cubical WildCat Algebra.AbGroups Homotopy.HSpace.Core TruncType Truncations.Core Truncations.Connectedness Homotopy.HomotopyGroup Homotopy.WhiteheadsPrinciple