`{Univalence} (X : pType) (n : nat) `{IsConnected n.+1 X} : pTr n.+2 (psusp (loops X)) <~>* pTr n.+2 X. Proof. snrapply Build_pEquiv. 1: rapply (fmap (pTr _) (loop_susp_counit _)). nrapply O_inverts_conn_map. nrapply (isconnmap_pred_add n.-2). rewrite 2 trunc_index_add_succ. rapply (conn_map_loop_susp_counit 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.