`{Univalence} {X : pType} `{IsHSpace X} `{forall a, IsEquiv (a *.)} : forall x y : X, transport (hopf_construction X) (merid x) y = x * y. Proof. intros x y. transport_to_ap. refine (ap (fun z => transport idmap z y) _ @ _). 1: apply Susp_rec_beta_merid. apply transport_path_universe. 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.