B G -> B G -> B G. Proof. intro b. snrapply ClassifyingSpace_rec. 1: exact _. 1: exact b. { intro x. revert b. snrapply ClassifyingSpace_ind_hset. 1: exact _. 1: exact (bloop x). cbn; intro y. apply dp_paths_lr. refine (concat_pp_p _ _ _ @ _). apply moveR_Vp. refine ((bloop_pp _ _)^ @ _ @ bloop_pp _ _). apply ap, commutativity. } intros x y. revert b. srapply ClassifyingSpace_ind_hprop. exact (bloop_pp x y). 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.