diff options
| author | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2025-11-05 08:11:48 -0600 |
|---|---|---|
| committer | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2025-11-05 08:11:48 -0600 |
| commit | 5f4d1cf740591476d3c7bc270fd11a2c578ab7e6 (patch) | |
| tree | 18e541e617682773e76041166cd516d9fe9dd668 /Functor/Monoidal/Construction/MultisetOf.agda | |
| parent | 0ce2b2ee7bc6f37473de60d801391dd3ff2dc024 (diff) | |
Adjust universe levels
Diffstat (limited to 'Functor/Monoidal/Construction/MultisetOf.agda')
| -rw-r--r-- | Functor/Monoidal/Construction/MultisetOf.agda | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/Functor/Monoidal/Construction/MultisetOf.agda b/Functor/Monoidal/Construction/MultisetOf.agda index 6862b84..eca7b3a 100644 --- a/Functor/Monoidal/Construction/MultisetOf.agda +++ b/Functor/Monoidal/Construction/MultisetOf.agda @@ -10,9 +10,9 @@ open import Category.Construction.CMonoids using (CMonoids) open import Level using (Level) module Functor.Monoidal.Construction.MultisetOf - {o ℓ e : Level} + {o o′ ℓ ℓ′ e e′ : Level} {𝒞 : CocartesianCategory o ℓ e} - {S : SymmetricMonoidalCategory o ℓ e} + {S : SymmetricMonoidalCategory o′ ℓ′ e′} (let module 𝒞 = CocartesianCategory 𝒞) (let module S = SymmetricMonoidalCategory S) (G : Functor 𝒞.U S.U) |