proposition: Theorem natequiv_grp_homo_pmap_bg `{U : Univalence} (G : Group) : NatEquiv (opyon G) (opyon (B G) o B).
proof: Proof. rapply Build_NatEquiv. Defined.
imports: Basics Types Pointed Cubical WildCat Algebra.AbGroups Homotopy.HSpace.Core TruncType Truncations.Core Truncations.Connectedness Homotopy.HomotopyGroup Homotopy.WhiteheadsPrinciple