proposition: Proposition hopf_retraction `{Univalence} (X : pType) `{IsHSpace X} `{forall a, IsEquiv (a *.)} : connecting_map_family (hopf_construction X) o* loop_susp_unit X ==* pmap_idmap.
proof: 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.
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