diff options
| author | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2025-12-06 16:53:08 -0600 |
|---|---|---|
| committer | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2025-12-06 16:53:08 -0600 |
| commit | 826b0b6007249ef518c5cff458ce6dc5c95fd43a (patch) | |
| tree | 9413a1421d520f5d24635b670832c7994b18d255 /Functor/Forgetful/Instance/Monoid.agda | |
| parent | 70fbd45702021e14b93bc294c4c1fa02c5c4758e (diff) | |
Update free and forgetful monoid functors
Diffstat (limited to 'Functor/Forgetful/Instance/Monoid.agda')
| -rw-r--r-- | Functor/Forgetful/Instance/Monoid.agda | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/Functor/Forgetful/Instance/Monoid.agda b/Functor/Forgetful/Instance/Monoid.agda index 2c786ef..2f9e4d8 100644 --- a/Functor/Forgetful/Instance/Monoid.agda +++ b/Functor/Forgetful/Instance/Monoid.agda @@ -1,23 +1,25 @@ {-# OPTIONS --without-K --safe #-} -open import Categories.Category.Monoidal using (MonoidalCategory) +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 : MonoidalCategory o ℓ e) where +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) -module S = MonoidalCategory S +private + module S = Category S open Monoid open Monoid⇒ open S.Equiv using (refl) open Functor -Forget : Functor (Monoids S.monoidal) S.U +Forget : Functor (Monoids monoidal) S Forget .F₀ = Carrier Forget .F₁ = arr Forget .identity = refl |