proposition: Lemma transport_hopf_construction `{Univalence} {X : pType} `{IsHSpace X} `{forall a, IsEquiv (a *.)} : forall x y : X, transport (hopf_construction X) (merid x) y = x * y.
proof: 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.
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