`{Univalence} {m : trunc_index} (X : pType) `{IsConnected m.+2 X} (k := (m.+1 +2+ m.+1).+1) `{IsHSpace X} `{IsTrunc k X} : X <~>* pTr k (loops (psusp X)). Proof. refine (_ o*E pequiv_ptr (n:=k)). nrefine (pequiv_O_inverts k (loop_susp_unit X)). rapply freudenthal_hspace. Defined.
Require Import Types Basics Pointed Truncations. Require Import HSpace Suspension ExactSequence HomotopyGroup. Require Import WildCat.Core WildCat.Universe WildCat.Equiv Modalities.ReflectiveSubuniverse Modalities.Descent. Require Import HSet Spaces.Nat.Core. Require Import Homotopy.Join Colimits.Pushout.