Add category of commutative monoids

1 files changed, 57 insertions, 0 deletions

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