From c9da00d8069d77bc4cd253d1197983e87edd1d6f Mon Sep 17 00:00:00 2001
From: Jacques Comeaux <jacquesrcomeaux@protonmail.com>
Date: Wed, 10 Dec 2025 13:38:10 -0600
Subject: Add free/forget multiset adjunction

---
 Functor/Forgetful/Instance/CMonoid.agda | 36 +++++++++++++++++++++++++++++++++
 1 file changed, 36 insertions(+)
 create mode 100644 Functor/Forgetful/Instance/CMonoid.agda

(limited to 'Functor/Forgetful/Instance/CMonoid.agda')

diff --git a/Functor/Forgetful/Instance/CMonoid.agda b/Functor/Forgetful/Instance/CMonoid.agda
new file mode 100644
index 0000000..fd8ecc1
--- /dev/null
+++ b/Functor/Forgetful/Instance/CMonoid.agda
@@ -0,0 +1,36 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Categories.Category using (Category)
+open import Categories.Category.Monoidal using (Monoidal)
+open import Categories.Category.Monoidal.Symmetric using (Symmetric)
+open import Level using (Level)
+
+module Functor.Forgetful.Instance.CMonoid
+    {o ℓ e : Level}
+    {S : Category o ℓ e}
+    {monoidal : Monoidal S}
+    (symmetric : Symmetric monoidal)
+  where
+
+open import Categories.Category.Construction.Monoids monoidal using (Monoids)
+open import Categories.Functor using (Functor)
+open import Category.Construction.CMonoids symmetric using (CMonoids)
+open import Function using (id)
+open import Object.Monoid.Commutative using (CommutativeMonoid; CommutativeMonoid⇒)
+
+private
+  module S = Category S
+
+open CommutativeMonoid
+open CommutativeMonoid⇒
+open Functor
+open S.Equiv using (refl)
+
+Forget : Functor CMonoids Monoids
+Forget .F₀ = monoid
+Forget .F₁ = monoid⇒
+Forget .identity = refl
+Forget .homomorphism = refl
+Forget .F-resp-≈ = id
+
+module Forget = Functor Forget
-- 
cgit v1.2.3