diff options
Diffstat (limited to 'Functor/Monoidal/Construction')
| -rw-r--r-- | Functor/Monoidal/Construction/MonoidValued.agda (renamed from Functor/Monoidal/Construction/FamilyOfMonoids.agda) | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/Functor/Monoidal/Construction/FamilyOfMonoids.agda b/Functor/Monoidal/Construction/MonoidValued.agda index 377342a..937714d 100644 --- a/Functor/Monoidal/Construction/FamilyOfMonoids.agda +++ b/Functor/Monoidal/Construction/MonoidValued.agda @@ -11,7 +11,7 @@ open import Level using (Level; _ā_) -- A functor from a cocartesian category š to Monoids[S] -- can be turned into a monoidal functor from š to S -module Functor.Monoidal.Construction.FamilyOfMonoids +module Functor.Monoidal.Construction.MonoidValued {o oā² ā āā² e eā² : Level} {š : Category o ā e} (š-+ : Cocartesian š) @@ -33,7 +33,7 @@ open import Categories.Functor.Properties using ([_]-resp-square; [_]-resp-ā) open import Categories.Morphism using (_ā
_) open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper) open import Data.Product using (_,_) -open import Functor.Forgetful.Instance.Monoid S using (Forget) +open import Functor.Forgetful.Instance.Monoid S.monoidal using (Forget) private |