diff options
Diffstat (limited to 'Functor/Forgetful/Instance/Monoid.agda')
| -rw-r--r-- | Functor/Forgetful/Instance/Monoid.agda | 27 |
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 |