diff options
Diffstat (limited to 'Category')
| -rw-r--r-- | Category/Instance/Setoids/SymmetricMonoidal.agda | 21 |
1 files changed, 10 insertions, 11 deletions
diff --git a/Category/Instance/Setoids/SymmetricMonoidal.agda b/Category/Instance/Setoids/SymmetricMonoidal.agda index fa4d903..8f448dc 100644 --- a/Category/Instance/Setoids/SymmetricMonoidal.agda +++ b/Category/Instance/Setoids/SymmetricMonoidal.agda @@ -1,33 +1,32 @@ {-# OPTIONS --without-K --safe #-} -module Category.Instance.Setoids.SymmetricMonoidal {ℓ} where +open import Level using (Level; _⊔_; suc) +module Category.Instance.Setoids.SymmetricMonoidal {c ℓ : Level} where -open import Categories.Category.Cartesian.Monoidal using (module CartesianMonoidal) open import Categories.Category.Instance.Setoids using (Setoids) open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory) open import Categories.Category.Monoidal.Instance.Setoids using (Setoids-Cartesian; Setoids-Cocartesian) renaming (Setoids-Monoidal to ×-monoidal) -open import Categories.Category.Cartesian.SymmetricMonoidal (Setoids ℓ ℓ) Setoids-Cartesian +open import Categories.Category.Cartesian.SymmetricMonoidal (Setoids c ℓ) Setoids-Cartesian using () renaming (symmetric to ×-symmetric) -open import Level using (suc) -open import Categories.Category.Cocartesian (Setoids ℓ ℓ) +open import Categories.Category.Cocartesian (Setoids c (c ⊔ ℓ)) using (module CocartesianMonoidal; module CocartesianSymmetricMonoidal) -open CocartesianMonoidal (Setoids-Cocartesian {ℓ} {ℓ}) using (+-monoidal) -open CocartesianSymmetricMonoidal (Setoids-Cocartesian {ℓ} {ℓ}) using (+-symmetric) +open CocartesianMonoidal (Setoids-Cocartesian {c} {ℓ}) using (+-monoidal) +open CocartesianSymmetricMonoidal (Setoids-Cocartesian {c} {ℓ}) using (+-symmetric) -Setoids-× : SymmetricMonoidalCategory (suc ℓ) ℓ ℓ +Setoids-× : SymmetricMonoidalCategory (suc (c ⊔ ℓ)) (c ⊔ ℓ) (c ⊔ ℓ) Setoids-× = record - { U = Setoids ℓ ℓ + { U = Setoids c ℓ ; monoidal = ×-monoidal ; symmetric = ×-symmetric } -Setoids-+ : SymmetricMonoidalCategory (suc ℓ) ℓ ℓ +Setoids-+ : SymmetricMonoidalCategory (suc (c ⊔ ℓ)) (c ⊔ ℓ) (c ⊔ ℓ) Setoids-+ = record - { U = Setoids ℓ ℓ + { U = Setoids c (c ⊔ ℓ) ; monoidal = +-monoidal ; symmetric = +-symmetric } |