1 files changed, 91 insertions, 0 deletions
diff --git a/Category/Instance/CMonoids.agda b/Category/Instance/CMonoids.agda
new file mode 100644
index 0000000..79bb032
--- /dev/null
+++ b/Category/Instance/CMonoids.agda
@@ -0,0 +1,91 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Level using (Level; suc; _⊔_)
+
+module Category.Instance.CMonoids (c ℓ : Level) where
+
+import Algebra.Morphism.Bundles as Raw
+import Algebra.Morphism.Construct.Composition as Compose
+import Algebra.Morphism.Construct.Identity as Identity
+
+open import Algebra using (CommutativeMonoid)
+open import Categories.Category using (Category)
+open import Categories.Category.Helper using (categoryHelper)
+open import Relation.Binary using (IsEquivalence)
+open import Function using (Func; _⟶ₛ_)
+
+open CommutativeMonoid hiding (_≈_)
+open Func
+
+record CMonoidHomomorphism (M N : CommutativeMonoid c ℓ) : Set (c ⊔ ℓ) where
+
+  constructor mk-⇒
+
+  field
+    rawMonoidHomomorphism : Raw.MonoidHomomorphism (rawMonoid M) (rawMonoid N)
+
+  open Raw.MonoidHomomorphism rawMonoidHomomorphism public
+
+  func : setoid M ⟶ₛ setoid N
+  func .to = ⟦_⟧
+  func .cong = ⟦⟧-cong
+
+module _ {M N : CommutativeMonoid c ℓ} where
+
+  -- Pointwise equality of monoid homomorphisms
+
+  open CMonoidHomomorphism
+
+  _≗_ : (f g : CMonoidHomomorphism M N) → Set (c ⊔ ℓ)
+  _≗_ f g = (x : Carrier M) → let open CommutativeMonoid N in ⟦ f ⟧ x ≈ ⟦ g ⟧ x
+
+  infix 4 _≗_
+
+  ≗-isEquivalence : IsEquivalence _≗_
+  ≗-isEquivalence = record
+      { refl = λ x → refl N
+      ; sym = λ f≈g x → sym N (f≈g x)
+      ; trans = λ f≈g g≈h x → trans N (f≈g x) (g≈h x)
+      }
+
+  module ≗ = IsEquivalence ≗-isEquivalence
+
+private
+
+  id : {M : CommutativeMonoid c ℓ} → CMonoidHomomorphism M M
+  id {M} = mk-⇒ record
+      { isMonoidHomomorphism = Identity.isMonoidHomomorphism (rawMonoid M) (refl M)
+      }
+
+  compose
+      : {M N P : CommutativeMonoid c ℓ}
+      → CMonoidHomomorphism N P
+      → CMonoidHomomorphism M N
+      → CMonoidHomomorphism M P
+  compose {P = P} f g = mk-⇒ record
+      { isMonoidHomomorphism =
+          Compose.isMonoidHomomorphism
+              (trans P)
+              g.isMonoidHomomorphism
+              f.isMonoidHomomorphism
+      }
+    where
+      module f = CMonoidHomomorphism f
+      module g = CMonoidHomomorphism g
+
+open CMonoidHomomorphism
+
+-- the category of commutative monoids and monoid homomorphisms
+CMonoids : Category (suc (c ⊔ ℓ)) (c ⊔ ℓ) (c ⊔ ℓ)
+CMonoids = categoryHelper record
+    { Obj = CommutativeMonoid c ℓ
+    ; _⇒_ = CMonoidHomomorphism
+    ; _≈_ = _≗_
+    ; id = id
+    ; _∘_ = compose
+    ; assoc = λ {_ _ _ Q} _ → refl Q
+    ; identityˡ = λ {_ B} _ → refl B
+    ; identityʳ = λ {_ B} _ → refl B
+    ; equiv = ≗-isEquivalence
+    ; ∘-resp-≈ = λ {C = C} {f g h i} eq₁ eq₂ x → trans C (⟦⟧-cong f (eq₂ x)) (eq₁ (⟦ i ⟧ x))
+    }