From 05cbf6f56bce1d45876630fe29b694dc57942e9c Mon Sep 17 00:00:00 2001
From: Jacques Comeaux <jacquesrcomeaux@protonmail.com>
Date: Thu, 13 Nov 2025 13:24:21 -0600
Subject: Add adjunction between free monoid and forget

---
 Data/Monoid.agda | 66 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 66 insertions(+)
 create mode 100644 Data/Monoid.agda

(limited to 'Data/Monoid.agda')

diff --git a/Data/Monoid.agda b/Data/Monoid.agda
new file mode 100644
index 0000000..ae2ded9
--- /dev/null
+++ b/Data/Monoid.agda
@@ -0,0 +1,66 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Level using (Level)
+module Data.Monoid {c ℓ : Level} where
+
+open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory)
+open import Category.Instance.Setoids.SymmetricMonoidal {c} {ℓ} using (Setoids-×)
+open import Categories.Object.Monoid using (Monoid; Monoid⇒)
+
+module Setoids-× = SymmetricMonoidalCategory Setoids-×
+
+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′; _,_)
+open Func
+
+-- A monoid object in the (monoidal) category of setoids is just a monoid
+
+toMonoid : Monoid Setoids-×.monoidal → Alg.Monoid c ℓ
+toMonoid M = record
+    { Carrier = Carrier
+    ; _≈_ = _≈_
+    ; _∙_ = curry′ (to μ)
+    ; ε = to η _
+    ; isMonoid = record
+        { isSemigroup = record
+            { isMagma = record
+                { isEquivalence = isEquivalence
+                ; ∙-cong = curry′ (cong μ)
+                }
+            ; assoc = λ x y z → assoc {(x , y) , z}
+            }
+        ; identity = (λ x → sym (identityˡ {_ , x}) ) , λ x → sym (identityʳ {x , _})
+        }
+    }
+  where
+    open Monoid M renaming (Carrier to A)
+    open Setoid A
+
+-- A morphism of monoids in the (monoidal) category of setoids is a monoid homomorphism
+
+module  _ (M N : Monoid Setoids-×.monoidal) where
+
+  module M = Alg.Monoid (toMonoid M)
+  module N = Alg.Monoid (toMonoid N)
+
+  open import Data.Product using (Σ; _,_)
+  open import Function using (_⟶ₛ_; _⟨$⟩_)
+  open import Algebra.Morphism using (IsMonoidHomomorphism)
+  open Monoid⇒
+  toMonoid⇒
+      : Monoid⇒ Setoids-×.monoidal M N
+      → Σ (M.setoid ⟶ₛ N.setoid) (λ f
+      → IsMonoidHomomorphism M.rawMonoid N.rawMonoid (to f))
+  toMonoid⇒ f = arr f , record
+      { isMagmaHomomorphism = record
+          { isRelHomomorphism = record
+              { cong = cong (arr f)
+              }
+          ; homo = λ x y → preserves-μ f {x , y}
+          }
+      ; ε-homo = preserves-η f
+      }
-- 
cgit v1.2.3