wip: should commAlgebraFromCommRing be a strict section of CommAlgebr…

…a→CommRing ?

Cubical/Algebra/CommAlgebra/Base.agda

@@ -140,7 +140,22 @@ module _ {R : CommRing ℓ} where
       commalgebrastr 0r 1S _+_ _·_  -_ _⋆_
         (makeIsCommAlgebra is-set +Assoc +Rid +Rinv +Comm ·Assoc ·Lid ·Ldist+ ·Comm
                                   ·Assoc⋆ ⋆DistR ⋆DistL ⋆Lid ⋆Assoc·)
-
+    {-
+      Would like to have
+        CommAlgebra→CommRing (commAlgebraFromCommRing S ...) ≡ S
+      definitionally.
+      How many records with no-eta does a CommRing contain? Two instances of IsSemigroup.
+    -}
+    module _
+      (_⋆_ : fst R → fst S → fst S)
+      (·Assoc⋆ : (r s : fst R) (x : fst S) → (r ·R s) ⋆ x ≡ r ⋆ (s ⋆ x))
+      (⋆DistR : (r s : fst R) (x : fst S) → (r +R s) ⋆ x ≡ (r ⋆ x) + (s ⋆ x))
+      (⋆DistL : (r : fst R) (x y : fst S) → r ⋆ (x + y) ≡ (r ⋆ x) + (r ⋆ y))
+      (⋆Lid : (x : fst S) → 1R ⋆ x ≡ x)
+      (⋆Assoc· : (r : fst R) (x y : fst S) → (r ⋆ x) · y ≡ r ⋆ (x · y))
+      where private
+      test : CommAlgebra→CommRing (commAlgebraFromCommRing _⋆_ ·Assoc⋆ ⋆DistR ⋆DistL ⋆Lid ⋆Assoc·) ≡ S
+      test = {! refl !}
 
   IsCommAlgebraEquiv : {A : Type ℓ'} {B : Type ℓ''}
     (M : CommAlgebraStr R A) (e : A ≃ B) (N : CommAlgebraStr R B)

Cubical/Algebra/CommAlgebra/QuotientAlgebra.agda

@@ -172,6 +172,16 @@ module _ {R : CommRing ℓ} (A : CommAlgebra R ℓ) where
        → (a : fst A) → fst (A / I)
 [ a ]/ = [ a ]
 
+
+
+module idealIsKernel {R : CommRing ℓ} (A : CommAlgebra R ℓ) (I : IdealsIn A) where
+
+  π = quotientHom A I
+
+  kernel≡I : kernel A (A / I) π ≡ I
+  kernel≡I = {!CommRing.idealIsKernel.kernel≡I!} -- cong Ideal→CommIdeal (Ring.idealIsKernel.kernel≡I (CommIdeal→Ideal I))
+
+
 private
   module _ (R : CommRing ℓ) where
     open CommRingStr (snd R)