(G : Group) (n : nat) : pType := match n with | 0 => G | 1 => pClassifyingSpace G | m.+1 => pTr m.+1 (psusp ( G m)) end. Notation "'K(' G , n )" := ( G n). Section . Context `{Univalence}. Global Instance istrunc_em {G : Group} {n : nat} : IsTrunc n K(G, n). Proof. destruct n as [|[]]; exact _. Defined.
Require Import Basics Types. Require Import Pointed. Require Import Cubical.DPath. Require Import Algebra.AbGroups. Require Import Homotopy.Suspension. Require Import Homotopy.ClassifyingSpace. Require Import Homotopy.HSpace.Coherent. Require Import Homotopy.HomotopyGroup. Require Import Homotopy.Hopf. Require Import Truncations.Core Truncations.Connectedness. Require Import WildCat.