proposition: Lemma pequiv_loops_em_em (G : AbGroup) (n : nat) : K(G, n) <~>* loops K(G, n.+1).
proof: Proof. destruct n. 1: apply pequiv_g_loops_bg. change (K(G, n.+1) <~>* loops (pTr n.+2 (psusp (K(G, n.+1))))). refine (ptr_loops _ _ o*E _). destruct n. 1: srapply (licata_finster (m:=-2)). refine (_ o*E pequiv_ptr (n:=n.+2)). rapply pequiv_ptr_loop_psusp'. Defined.
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