forall x y, bg_mul x y = bg_mul y x. Proof. intros x. srapply ClassifyingSpace_ind_hset. { simpl. revert x. srapply ClassifyingSpace_ind_hset. 1: reflexivity. intros x. apply sq_dp^-1, sq_1G. refine (ap_idmap _ @ _^). nrapply ClassifyingSpace_rec_beta_bloop. } intros y; revert x. simpl. snrapply ClassifyingSpace_ind_hprop. 1: exact _. simpl. nrapply (transport_paths_FFlr' (g := idmap)). apply equiv_p1_1q. lhs nrapply ap_idmap. nrapply ClassifyingSpace_rec_beta_bloop. 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.