proposition: Proposition isequiv_Pi_connected_hspace `{Univalence} {n : nat} (X : pType) `{IsConnected n X} `{IsHSpace X} : IsEquiv (fmap (pPi (n + n).+1) (loop_susp_unit X)).
proof: 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.
imports: Types Basics Pointed Truncations HSpace Suspension ExactSequence HomotopyGroup WildCat.Core WildCat.Universe WildCat.Equiv Modalities.ReflectiveSubuniverse Modalities.Descent HSet Spaces.Nat.Core Homotopy.Join Colimits.Pushout