proposition: Theorem equiv_grp_homo_pmap_bg `{U : Univalence} (G H : Group) : (G $-> H) <~> (B G $-> B H).
proof: Proof. snrapply Build_Equiv. 2: apply isequiv_fmap_pclassifyingspace. Defined.
imports: Basics Types Pointed Cubical WildCat Algebra.AbGroups Homotopy.HSpace.Core TruncType Truncations.Core Truncations.Connectedness Homotopy.HomotopyGroup Homotopy.WhiteheadsPrinciple