{G : AbGroup} (n : nat) : IsCohHSpace K(G, n). Proof. nrapply iscohhspace_equiv_cohhspace. 2: apply pequiv_loops_em_em. apply iscohhspace_loops. 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.