(P : ClassifyingSpace G -> Type) `{forall b, IsTrunc 1 (P b)} (bbase' : P bbase) (bloop' : forall x, DPath P (bloop x) bbase' bbase') (bloop_pp' : forall x y, DPathSquare P (sq_G1 (bloop_pp x y)) (bloop' (x * y)) ((bloop' x) @Dp (bloop' y)) 1 1) (x : G) : apD (ClassifyingSpace_ind P bbase' bloop' bloop_pp') (bloop x) = bloop' x. Proof. Admitted. End ClassifyingSpace_ind. End ClassifyingSpace. Section Eliminators. Context {G : Group}.
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.