`{Univalence} (X : pType) : pfiber (loop_susp_counit X) <~>* pjoin (loops X) (loops X). Proof. snrefine (pequiv_hopf_total_join (loops X) o*E _). 2: rapply ishspace_loops. 2,3: exact _. snrapply Build_pEquiv'. { snrapply equiv_functor_sigma'. 1: exact (emap psusp (equiv_path_inverse _ _)). snrapply Susp_ind; hnf. 1,2: reflexivity. intros p. nrapply path_equiv. funext q. simpl. lhs rapply (transport_equiv (merid p) _ q). simpl. lhs nrapply ap. { lhs nrapply transport_paths_Fl. nrapply whiskerR. { lhs nrapply (ap inverse (ap_V _ _)). lhs rapply inv_V. apply Susp_rec_beta_merid. } } lhs nrapply (transport_idmap_ap _ (merid p)). lhs nrapply (transport2 idmap). { lhs nrapply ap_compose. lhs nrapply ap. 1: apply functor_susp_beta_merid. apply Susp_rec_beta_merid. } lhs nrapply transport_path_universe. apply concat_V_pp. } 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.