From 9ce0effed3bad94089fa3cbb5a8968330341191a Mon Sep 17 00:00:00 2001
From: Felix Cherubini <felix.cherubini@posteo.de>
Date: Mon, 26 Aug 2024 16:39:08 +0200
Subject: [PATCH] more boilterplate, morphism contructor

---
 Cubical/Algebra/CommAlgebra/Base.agda       | 15 +++++++--
 Cubical/Algebra/CommAlgebra/Properties.agda | 34 +++++++++++++++++++++
 2 files changed, 46 insertions(+), 3 deletions(-)

diff --git a/Cubical/Algebra/CommAlgebra/Base.agda b/Cubical/Algebra/CommAlgebra/Base.agda
index 2cd055567..10668f649 100644
--- a/Cubical/Algebra/CommAlgebra/Base.agda
+++ b/Cubical/Algebra/CommAlgebra/Base.agda
@@ -138,9 +138,9 @@ module _ {R : CommRing ℓ} where
   idCommAlgebraHom = idCAlgHom
 
   compCommAlgebraHom : {A : CommAlgebra R ℓ'} {B : CommAlgebra R ℓ''} {C : CommAlgebra R ℓ'''}
-                      → (g : CommAlgebraHom B C) → (f : CommAlgebraHom A B)
+                      → (f : CommAlgebraHom A B) → (g : CommAlgebraHom B C)
                       → CommAlgebraHom A C
-  compCommAlgebraHom {A = A} {B = B} {C = C} g f =
+  compCommAlgebraHom {A = A} {B = B} {C = C} f g =
     CommRingHom→CommAlgebraHom (⟨ g ⟩ᵣ→ ∘cr ⟨ f ⟩ᵣ→) pasting
     where
       opaque
@@ -160,7 +160,7 @@ module _ {R : CommRing ℓ} where
   infixr 9 _∘ca_ -- same as functions
   _∘ca_ : {A : CommAlgebra R ℓ'} {B : CommAlgebra R ℓ''} {C : CommAlgebra R ℓ'''}
         → CommAlgebraHom B C → CommAlgebraHom A B → CommAlgebraHom A C
-  g ∘ca f = compCommAlgebraHom g f
+  g ∘ca f = compCommAlgebraHom f g
 
   opaque
     CommAlgebraHom≡ :
@@ -227,6 +227,15 @@ module _ {R : CommRing ℓ} where
   CommAlgebra→CommRingStr : (A : CommAlgebra R ℓ') → CommRingStr ⟨ A ⟩ₐ
   CommAlgebra→CommRingStr A = A .fst .snd
 
+  CommAlgebra→Set : (A : CommAlgebra R ℓ') → hSet ℓ'
+  CommAlgebra→Set A = ⟨ A ⟩ₐ , is-set
+    where open CommRingStr (CommAlgebra→CommRingStr A) using (is-set)
+
+  isSetCommAlgebraHom : (A : CommAlgebra R ℓ') (B : CommAlgebra R ℓ'')
+                        → isSet (CommAlgebraHom A B)
+  isSetCommAlgebraHom A B = isSetΣSndProp (isSet→ is-set) (λ _ → isPropIsCommAlgebraHom _ _ _)
+    where open CommRingStr (CommAlgebra→CommRingStr B) using (is-set)
+
   CommAlgebraHom→RingHom : {A : CommAlgebra R ℓ'} {B : CommAlgebra R ℓ''}
                              → CommAlgebraHom A B
                              → RingHom (CommAlgebra→Ring A) (CommAlgebra→Ring B)
diff --git a/Cubical/Algebra/CommAlgebra/Properties.agda b/Cubical/Algebra/CommAlgebra/Properties.agda
index 0cf21ba7a..068fb4652 100644
--- a/Cubical/Algebra/CommAlgebra/Properties.agda
+++ b/Cubical/Algebra/CommAlgebra/Properties.agda
@@ -46,3 +46,37 @@ module _ {R : CommRing ℓ} where
                 f⁻¹ .fst .fst ∘ B .snd .fst                ≡⟨ sym ( cong ((f⁻¹ .fst .fst) ∘_) (cong fst (IsCommAlgebraHom.commutes (f .snd)))) ⟩
                 f⁻¹ .fst .fst ∘  f .fst .fst ∘ A .snd .fst ≡⟨ cong (_∘ A .snd .fst) f⁻¹∘f≡Id  ⟩
                 A .snd .fst ∎
+
+module _
+  -- Variable generalization would fail below without the module parameters A and B.
+  {R : CommRing ℓ}
+  {A : CommAlgebra R ℓ'}
+  {B : CommAlgebra R ℓ''}
+  {f : ⟨ A ⟩ₐ → ⟨ B ⟩ₐ}
+  where
+
+  open CommAlgebraStr ⦃...⦄
+  open CommRingStr ⦃...⦄
+  private instance
+    _ = CommAlgebra→CommRingStr A
+    _ = CommAlgebra→CommRingStr B
+    _ = CommAlgebra→CommAlgebraStr A
+    _ = CommAlgebra→CommAlgebraStr B
+
+  module _
+    (p1 : f 1r ≡ 1r)
+    (p+ : (x y : ⟨ A ⟩ₐ) → f (x + y) ≡ f x + f y)
+    (p· : (x y : ⟨ A ⟩ₐ) → f (x · y) ≡ f x · f y)
+    (p⋆ : (r : ⟨ R ⟩) (x : ⟨ A ⟩ₐ) → f (r ⋆ x) ≡ r ⋆ f x)
+    where
+
+    makeIsCommAlgebraHom : IsCommAlgebraHom A B f
+    makeIsCommAlgebraHom .IsCommAlgebraHom.isCommRingHom = makeIsCommRingHom p1 p+ p·
+    makeIsCommAlgebraHom .IsCommAlgebraHom.commutes =
+      CommRingHom≡ $ funExt λ r → f (A .snd .fst r)        ≡⟨ cong f (sym (·IdR _)) ⟩
+                                  f ((A .snd .fst r) · 1r) ≡⟨⟩
+                                  f (r ⋆ 1r)               ≡⟨ p⋆ _ _ ⟩
+                                  r ⋆ (f 1r)               ≡⟨⟩
+                                  (B .snd .fst r) · f 1r   ≡⟨ cong ((B .snd .fst r) ·_) p1 ⟩
+                                  (B .snd .fst r) · 1r     ≡⟨ ·IdR _ ⟩
+                                  B .snd .fst r ∎