Add adjunction between free monoid and forget

1 files changed, 27 insertions, 0 deletions

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