`{Univalence} (X : pType) `{IsHSpace X} `{forall a, IsEquiv (a *.)} `{forall a, IsEquiv (.* a)} : psigma (hopf_construction X) <~>* pjoin X X. Proof. snrapply Build_pEquiv'. { refine (_ oE equiv_pushout_flatten (f := const_tt X) (g := const_tt X) (Unit_ind (pointed_type X)) (Unit_ind (pointed_type X)) (fun x => Build_Equiv _ _ (x *.) (H1 x))). snrapply equiv_pushout. { cbn. refine (equiv_sigma_prod0 _ _ oE _ oE equiv_sigma_symm0 _ _). snrapply equiv_functor_sigma_id. intros x. exact (Build_Equiv _ _ (.* x) _). } 1,2: rapply (equiv_contr_sigma (Unit_ind (pointed_type X))). 1,2: reflexivity. } reflexivity. 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.