From b68c3ab18a0247d1815869a3b27c8789ddc7ae48 Mon Sep 17 00:00:00 2001
From: Ali Caglayan <alizter@gmail.com>
Date: Mon, 8 Jan 2024 13:11:10 +0000
Subject: [PATCH 1/2] CayleyDickson: some cleanups, remove funext

Signed-off-by: Ali Caglayan <alizter@gmail.com>
---
 theories/Homotopy/CayleyDickson.v | 58 +++++++++++++++----------------
 1 file changed, 28 insertions(+), 30 deletions(-)

diff --git a/theories/Homotopy/CayleyDickson.v b/theories/Homotopy/CayleyDickson.v
index e9bfd29f336..fcfd6e84d6d 100644
--- a/theories/Homotopy/CayleyDickson.v
+++ b/theories/Homotopy/CayleyDickson.v
@@ -185,7 +185,7 @@ Defined.
 Section ImaginaroidHSpace.
 
   (* Let A be a Cayley-Dickson imaginaroid with associative H-space multiplication on Susp A *)
-  Context `{Funext} {A} `(CayleyDicksonImaginaroid A)
+  Context {A} `(CayleyDicksonImaginaroid A)
     `(!Associative hspace_op).
 
   (** Declaring these as local instances so that they can be found *)
@@ -249,26 +249,29 @@ Section ImaginaroidHSpace.
     : SgOp (pjoin (psusp A) (psusp A)).
   Proof.
     unfold psusp, pjoin; cbn.
+    intros x y; revert x.
     srapply Join_rec; hnf.
     { intro a.
+      revert y.
       srapply Join_rec; hnf.
       - intro c.
-        exact (joinl (hspace_op a c)).
+        exact (joinl (a * c)).
       - intro d.
-        exact (joinr (hspace_op (conj a) d)).
+        exact (joinr (conj a * d)).
       - intros x y.
         apply jglue. }
     { intro b.
+      revert y.
       srapply Join_rec; hnf.
       - intro c.
-        exact (joinr (hspace_op c b)).
+        exact (joinr (c * b)).
       - intro d.
-        exact (joinl (hspace_op (-d) (conj b))).
+        exact (joinl ((-d) * conj b)).
       - intros x y.
         symmetry.
         apply jglue. }
     intros a b.
-    apply path_forall.
+    revert y.
     srapply Join_ind_dp.
     1: intro; apply jglue.
     1: intro; cbn; symmetry; apply jglue.
@@ -301,37 +304,32 @@ Section ImaginaroidHSpace.
   Global Instance cd_op_left_identity
     : LeftIdentity cd_op pt.
   Proof.
-    srapply Join_ind_dp.
-    { unfold cd_op, Join_rec, Pushout.Pushout_rec, Pushout.Pushout_ind; simpl;
-        intro a; apply ap.
-      srapply hspace_left_identity. }
-    { unfold cd_op, Join_rec, Pushout.Pushout_rec, Pushout.Pushout_ind.
-      simpl; intro b; apply ap.
-      srapply hspace_left_identity. }
+    snrapply Join_ind_FFlr.
+    1,2: exact (fun _ => ap _ (hspace_left_identity _)).
     intros a b.
-     simpl. apply sq_dp^-1.
-    rewrite ap_idmap, Join_rec_beta_jglue.
-    apply join_natsq_v.
+    refine (whiskerR _ _ @ _).
+    { refine (ap _ (ap_idmap _) @ _).
+      exact (Join_rec_beta_jglue
+        (fun c => joinl (pt * c))
+        (fun d => joinr (conj pt * d))
+        (fun x y => jglue (pt * x) (conj pt * y))
+        a b). }
+    symmetry.
+    apply join_natsq.
   Defined.
 
   Global Instance cd_op_right_identity
     : RightIdentity cd_op pt.
   Proof.
-    srapply Join_ind_dp.
-    { unfold cd_op, Join_rec, Pushout.Pushout_rec, Pushout.Pushout_ind; simpl.
-      intro a; apply ap.
-      srapply hspace_right_identity. }
-    { unfold cd_op, Join_rec, Pushout.Pushout_rec, Pushout.Pushout_ind; simpl.
-      intro b; apply ap.
-      srapply hspace_left_identity. }
+    snrapply Join_ind_FFlr.
+    1: exact (fun _ => ap joinl (hspace_right_identity _)).
+    1: exact (fun _ => ap joinr (hspace_left_identity _)).
     intros a b.
-    apply sq_dp^-1.
-    rewrite ap_idmap.
-    rewrite (ap_compose _ (fun f => f _)).
-    rewrite Join_rec_beta_jglue.
-    rewrite ap_apply_l.
-    rewrite eisretr.
-    apply join_natsq_v.
+    refine (whiskerR _ _ @ _).
+    { refine (ap _ (ap_idmap _) @ _).
+      simpl; rapply Join_rec_beta_jglue. }
+    symmetry.
+    apply join_natsq.
   Defined.
 
   Global Instance hspace_cdi_susp_assoc

From 5efe1b96ab00ab0fab97c1a7fa53430459ba6020 Mon Sep 17 00:00:00 2001
From: Ali Caglayan <alizter@gmail.com>
Date: Mon, 8 Jan 2024 21:56:37 +0000
Subject: [PATCH 2/2] review comments

Signed-off-by: Ali Caglayan <alizter@gmail.com>
---
 theories/Homotopy/CayleyDickson.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/Homotopy/CayleyDickson.v b/theories/Homotopy/CayleyDickson.v
index fcfd6e84d6d..16855a735e4 100644
--- a/theories/Homotopy/CayleyDickson.v
+++ b/theories/Homotopy/CayleyDickson.v
@@ -307,8 +307,8 @@ Section ImaginaroidHSpace.
     snrapply Join_ind_FFlr.
     1,2: exact (fun _ => ap _ (hspace_left_identity _)).
     intros a b.
-    refine (whiskerR _ _ @ _).
-    { refine (ap _ (ap_idmap _) @ _).
+    lhs nrapply whiskerR.
+    { lhs refine (ap _ (ap_idmap _)).
       exact (Join_rec_beta_jglue
         (fun c => joinl (pt * c))
         (fun d => joinr (conj pt * d))