GroupIsomorphism G (LoopGroup (B G)). Proof. snrapply Build_GroupIsomorphism'. 1: exact equiv_g_loops_bg. intros x y. apply bloop_pp. Defined.
Require Import Basics Types. Require Import Pointed WildCat. Require Import Cubical.DPath Cubical.PathSquare Cubical.DPathSquare. Require Import Algebra.AbGroups. Require Import Homotopy.HSpace.Core. Require Import TruncType. Require Import Truncations.Core Truncations.Connectedness. Require Import Homotopy.HomotopyGroup. Require Import Homotopy.WhiteheadsPrinciple. Module Import ClassifyingSpaceNotation.