1 files changed, 77 insertions, 0 deletions
diff --git a/Data/CMonoid.agda b/Data/CMonoid.agda
new file mode 100644
index 0000000..8aaf869
--- /dev/null
+++ b/Data/CMonoid.agda
@@ -0,0 +1,77 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Level using (Level)
+module Data.CMonoid {c ℓ : Level} where
+
+open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory)
+open import Category.Instance.Setoids.SymmetricMonoidal {c} {ℓ} using (Setoids-×; ×-symmetric′)
+open import Object.Monoid.Commutative using (CommutativeMonoid; CommutativeMonoid⇒)
+open import Categories.Object.Monoid using (Monoid)
+
+open import Data.Monoid {c} {ℓ} using (toMonoid; fromMonoid; toMonoid⇒)
+
+import Algebra.Bundles as Alg
+
+open import Data.Setoid using (∣_∣)
+open import Relation.Binary using (Setoid)
+open import Function using (Func; _⟨$⟩_)
+open import Data.Product using (curry′; uncurry′; _,_)
+open Func
+
+-- A commutative monoid object in the (symmetric monoidal) category of setoids
+-- is just a commutative monoid
+
+toCMonoid : CommutativeMonoid Setoids-×.symmetric → Alg.CommutativeMonoid c ℓ
+toCMonoid M = record
+    { M
+    ; isCommutativeMonoid = record
+        { isMonoid = M.isMonoid
+        ; comm = comm
+        }
+    }
+  where
+    open CommutativeMonoid M using (monoid; commutative; μ)
+    module M = Alg.Monoid (toMonoid monoid)
+    opaque
+      unfolding toMonoid
+      comm : (x y : M.Carrier) → x M.∙ y M.≈ y M.∙ x
+      comm x y = commutative {x , y}
+
+open import Function.Construct.Constant using () renaming (function to Const)
+open import Data.Setoid.Unit using (⊤ₛ)
+
+fromCMonoid : Alg.CommutativeMonoid c ℓ → CommutativeMonoid Setoids-×.symmetric
+fromCMonoid M = record
+    { M
+    ; isCommutativeMonoid = record
+        { isMonoid = M.isMonoid
+        ; commutative = commutative
+        }
+    }
+  where
+    open Alg.CommutativeMonoid M using (monoid; comm)
+    module M = Monoid (fromMonoid monoid)
+    open Setoids-× using (_≈_; _∘_; module braiding)
+    opaque
+      unfolding toMonoid
+      commutative : M.μ ≈ M.μ ∘ braiding.⇒.η _
+      commutative {x , y} = comm x y
+
+-- A morphism of monoids in the (monoidal) category of setoids is a monoid homomorphism
+
+module  _ (M N : CommutativeMonoid Setoids-×.symmetric) where
+
+  module M = Alg.CommutativeMonoid (toCMonoid M)
+  module N = Alg.CommutativeMonoid (toCMonoid N)
+
+  open import Data.Product using (Σ; _,_)
+  open import Function using (_⟶ₛ_)
+  open import Algebra.Morphism using (IsMonoidHomomorphism)
+  open CommutativeMonoid
+  open CommutativeMonoid⇒
+
+  toCMonoid⇒
+      : CommutativeMonoid⇒ Setoids-×.symmetric M N
+      → Σ (M.setoid ⟶ₛ N.setoid) (λ f
+      → IsMonoidHomomorphism M.rawMonoid N.rawMonoid (to f))
+  toCMonoid⇒ f = toMonoid⇒ (monoid M) (monoid N) (monoid⇒ f)