`{Univalence} {m : trunc_index} (X : pType) `{IsConnected m.+2 X} `{IsHSpace X} : O_inverts (Tr (m.+1 +2+ m.+1).+1) (loop_susp_unit X). Proof. pose (is0connected_isconnected m _). exact (' (m:=m.+1) X). 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.