`{Univalence} {n : nat} (X : pType) `{IsConnected n X} `{IsHSpace X} : IsEquiv (fmap (pPi (n + n).+1) (loop_susp_unit X)). Proof. nrapply isequiv_surj_emb. - apply issurj_pi_connmap. destruct n. + by apply (conn_map_loop_susp_unit (-1)). + rewrite <- trunc_index_add_nat_add. by apply (conn_map_loop_susp_unit). - pose (is0connected_isconnected n.-2 _). nrapply isembedding_pi_psect. apply hopf_retraction. 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.