freudenthal_hspace' `{Univalence} {m : trunc_index} (X : pType) `{IsConnected m.+1 X} `{IsHSpace X} `{forall a, IsEquiv (a *.)} : O_inverts (Tr (m +2+ m).+1) (loop_susp_unit X). Proof. set (r:=connecting_map_family (hopf_construction X)). nrapply (OO_inverts_conn_map_factor_conn_map _ (m +2+ m) _ r). 2, 4: exact _. 1: apply O_lex_leq_Tr. rapply (conn_map_homotopic _ equiv_idmap (r o loop_susp_unit X)). symmetry. nrapply 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.