From 821832147fb2b3b06ebda7e991ad880eaba15bcc Mon Sep 17 00:00:00 2001
From: Jacques Comeaux <jacquesrcomeaux@protonmail.com>
Date: Wed, 5 Nov 2025 01:02:33 -0600
Subject: Add category of commutative monoids

---
 Category/Construction/CMonoids.agda | 57 +++++++++++++++++++++++++++++++++++++
 Object/Monoid/Commutative.agda      | 48 +++++++++++++++++++++++++++++++
 2 files changed, 105 insertions(+)
 create mode 100644 Category/Construction/CMonoids.agda
 create mode 100644 Object/Monoid/Commutative.agda

diff --git a/Category/Construction/CMonoids.agda b/Category/Construction/CMonoids.agda
new file mode 100644
index 0000000..c2793cf
--- /dev/null
+++ b/Category/Construction/CMonoids.agda
@@ -0,0 +1,57 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Categories.Category.Core using (Category)
+open import Categories.Category.Monoidal.Core using (Monoidal)
+open import Categories.Category.Monoidal.Symmetric using (Symmetric)
+open import Level using (Level; _⊔_)
+
+-- The category of commutative monoids internal to a symmetric monoidal category
+
+module Category.Construction.CMonoids
+  {o ℓ e : Level}
+  {𝒞 : Category o ℓ e}
+  {M : Monoidal 𝒞}
+  (symmetric : Symmetric M)
+  where
+
+open import Categories.Functor using (Functor)
+open import Categories.Morphism.Reasoning 𝒞
+open import Object.Monoid.Commutative symmetric
+
+open Category 𝒞
+open Monoidal M
+open HomReasoning
+open CommutativeMonoid⇒
+
+CMonoids : Category (o ⊔ ℓ ⊔ e) (ℓ ⊔ e) e
+CMonoids = record
+    { Obj = CommutativeMonoid
+    ; _⇒_ = CommutativeMonoid⇒
+    ; _≈_ = λ f g → arr f ≈ arr g
+    ; id = record
+        { monoid⇒ = record
+            { arr = id
+            ; preserves-μ = identityˡ ○ introʳ ⊗.identity
+            ; preserves-η = identityˡ
+            }
+        }
+    ; _∘_ = λ f g → record
+        { monoid⇒ = record
+            { arr = arr f ∘ arr g
+            ; preserves-μ = glue (preserves-μ f) (preserves-μ g) ○ ∘-resp-≈ʳ (⟺ ⊗.homomorphism)
+            ; preserves-η = glueTrianglesˡ (preserves-η f) (preserves-η g)
+            }
+        }
+    ; assoc = assoc
+    ; sym-assoc = sym-assoc
+    ; identityˡ = identityˡ
+    ; identityʳ = identityʳ
+    ; identity² = identity²
+    ; equiv = record
+      { refl = refl
+      ; sym = sym
+      ; trans = trans
+      }
+    ; ∘-resp-≈ = ∘-resp-≈
+    }
+  where open Equiv
diff --git a/Object/Monoid/Commutative.agda b/Object/Monoid/Commutative.agda
new file mode 100644
index 0000000..8a8c756
--- /dev/null
+++ b/Object/Monoid/Commutative.agda
@@ -0,0 +1,48 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Categories.Category.Core using (Category)
+open import Categories.Category.Monoidal.Core using (Monoidal)
+open import Categories.Category.Monoidal.Symmetric using (Symmetric)
+open import Level using (Level; _⊔_)
+
+module Object.Monoid.Commutative {o ℓ e : Level} {𝒞 : Category o ℓ e} {M : Monoidal 𝒞} (sym : Symmetric M) where
+
+open import Categories.Object.Monoid M using (IsMonoid; Monoid; Monoid⇒)
+
+-- a commutative monoid object in a symmetric monoidal category
+
+open Category 𝒞
+open Symmetric sym using (module braiding; _⊗₁_)
+
+record IsCommutativeMonoid (M : Obj) : Set (ℓ ⊔ e) where
+
+  field
+    isMonoid : IsMonoid M
+
+  open IsMonoid isMonoid public
+
+  field
+    commutative : μ ≈ μ ∘ braiding.⇒.η _
+
+record CommutativeMonoid : Set (o ⊔ ℓ ⊔ e) where
+
+  field
+    Carrier : Obj
+    isCommutativeMonoid : IsCommutativeMonoid Carrier
+
+  open IsCommutativeMonoid isCommutativeMonoid public
+
+  monoid : Monoid
+  monoid = record { isMonoid = isMonoid }
+
+open CommutativeMonoid
+
+record CommutativeMonoid⇒ (M M′ : CommutativeMonoid) : Set (ℓ ⊔ e) where
+
+  module M = CommutativeMonoid M
+  module M′ = CommutativeMonoid M′
+
+  field
+    monoid⇒ : Monoid⇒ M.monoid M′.monoid
+
+  open Monoid⇒ monoid⇒ public
-- 
cgit v1.2.3