`{Univalence} (X : pType) `{IsHSpace X} `{forall a, IsEquiv (a *.)} : connecting_map_family (hopf_construction X) o* loop_susp_unit X ==* pmap_idmap. Proof. nrapply hspace_phomotopy_from_homotopy. 1: assumption. intro x; cbn. refine (transport_pp _ _ _ _ @ _); unfold dpoint. apply moveR_transport_V. refine (transport_hopf_construction _ _ @ _ @ (transport_hopf_construction _ _)^). exact (right_identity _ @ (left_identity _)^). 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.