fact: Fixpoint EilenbergMacLane (G : Group) (n : nat) : pType := match n with | 0 => G | 1 => pClassifyingSpace G | m.+1 => pTr m.+1 (psusp (EilenbergMacLane G m)) end.
imports: Basics Types Pointed Cubical.DPath Algebra.AbGroups Homotopy.Suspension Homotopy.ClassifyingSpace Homotopy.HSpace.Core Homotopy.HSpace.Coherent Homotopy.HomotopyGroup Homotopy.Hopf TruncType Truncations.Core Truncations.Connectedness WildCat