(X : pType) (n : nat) `{IsConnected n X} `{IsTrunc n.+1 X} : K(Pi n.+1 X, n.+1) <~>* X. Proof. generalize dependent X; induction n; intros X isC isT. 1: rapply pequiv_pclassifyingspace_pi1. refine ((pequiv_ptr (n:=n.+2))^-1* o*E _). refine (pequiv_ptr_psusp_loops X n o*E _). change (K(?G, n.+2)) with (pTr n.+2 (psusp K( G, n.+1 ))). refine (emap (pTr n.+2 o psusp) _). refine ((IHn (loops X) _ _) o*E _). apply pequiv_em_group_iso. apply groupiso_pi_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.