2 files changed, 65 insertions, 0 deletions
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
diff --git a/Functor/Forgetful/Instance/Monoid.agda b/Functor/Forgetful/Instance/Monoid.agda
new file mode 100644
index 0000000..2f9e4d8
--- /dev/null
+++ b/Functor/Forgetful/Instance/Monoid.agda
@@ -0,0 +1,29 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Categories.Category using (Category)
+open import Categories.Category.Monoidal using (Monoidal)
+open import Level using (Level)
+
+module Functor.Forgetful.Instance.Monoid {o ℓ e : Level} {S : Category o ℓ e} (monoidal : Monoidal S) where
+
+open import Categories.Category.Construction.Monoids using (Monoids)
+open import Categories.Functor using (Functor)
+open import Categories.Object.Monoid using (Monoid; Monoid⇒)
+open import Function using (id)
+
+private
+  module S = Category S
+
+open Monoid
+open Monoid⇒
+open S.Equiv using (refl)
+open Functor
+
+Forget : Functor (Monoids monoidal) S
+Forget .F₀ = Carrier
+Forget .F₁ = arr
+Forget .identity = refl
+Forget .homomorphism = refl
+Forget .F-resp-≈ = id
+
+module Forget = Functor Forget