aboutsummaryrefslogtreecommitdiff
path: root/Category/Instance/Setoids
diff options
context:
space:
mode:
Diffstat (limited to 'Category/Instance/Setoids')
-rw-r--r--Category/Instance/Setoids/SymmetricMonoidal.agda4
1 files changed, 3 insertions, 1 deletions
diff --git a/Category/Instance/Setoids/SymmetricMonoidal.agda b/Category/Instance/Setoids/SymmetricMonoidal.agda
index 995ddf3..e6c04d5 100644
--- a/Category/Instance/Setoids/SymmetricMonoidal.agda
+++ b/Category/Instance/Setoids/SymmetricMonoidal.agda
@@ -12,7 +12,9 @@ open import Categories.Category.Cartesian.SymmetricMonoidal (Setoids c ℓ) Seto
using ()
renaming (symmetric to ×-symmetric)
open import Categories.Category.Cocartesian (Setoids c (c ⊔ ℓ))
- using (module CocartesianMonoidal; module CocartesianSymmetricMonoidal)
+open import Categories.Category.Cocartesian.Monoidal using (module CocartesianMonoidal)
+open import Categories.Category.Cocartesian.SymmetricMonoidal (Setoids c (c ⊔ ℓ))
+ using (module CocartesianSymmetricMonoidal)
open CocartesianMonoidal (Setoids-Cocartesian {c} {ℓ}) using (+-monoidal)
open CocartesianSymmetricMonoidal (Setoids-Cocartesian {c} {ℓ}) using (+-symmetric)