1 files changed, 27 insertions, 13 deletions
diff --git a/Category/Instance/Setoids/SymmetricMonoidal.agda b/Category/Instance/Setoids/SymmetricMonoidal.agda
index fa4d903..995ddf3 100644
--- a/Category/Instance/Setoids/SymmetricMonoidal.agda
+++ b/Category/Instance/Setoids/SymmetricMonoidal.agda
@@ -1,33 +1,47 @@
 {-# 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 ℓ) ℓ ℓ
+open import Categories.Category using (Category)
+open import Categories.Category.Monoidal using (Monoidal)
+open import Categories.Category.Monoidal.Symmetric using (Symmetric)
+
+opaque
+
+  ×-monoidal′ : Monoidal (Setoids c ℓ)
+  ×-monoidal′ = ×-monoidal {c} {ℓ}
+
+  ×-symmetric′ : Symmetric ×-monoidal′
+  ×-symmetric′ = ×-symmetric
+
+Setoids-× : SymmetricMonoidalCategory (suc (c ⊔ ℓ)) (c ⊔ ℓ) (c ⊔ ℓ)
 Setoids-× = record
-    { U = Setoids ℓ ℓ
-    ; monoidal = ×-monoidal
-    ; symmetric = ×-symmetric
+    { 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
     }
+
+module Setoids-× = SymmetricMonoidalCategory Setoids-×
+module Setoids-+ = SymmetricMonoidalCategory Setoids-+