diff options
Diffstat (limited to 'Functor/Forgetful/Instance/CMonoid.agda')
| -rw-r--r-- | Functor/Forgetful/Instance/CMonoid.agda | 36 |
1 files changed, 36 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 |