3 files changed, 14 insertions, 17 deletions

diff --git a/Category/Monoidal/Instance/Cospans.agda b/Category/Monoidal/Instance/Cospans.agda
index a1648db..187eaca 100644
--- a/Category/Monoidal/Instance/Cospans.agda
+++ b/Category/Monoidal/Instance/Cospans.agda
@@ -9,9 +9,9 @@ import Categories.Morphism as Morphism
 import Categories.Morphism.Reasoning.Iso as IsoReasoning
 
 open import Categories.Category using (_[_,_]; _[_≈_]; _[_∘_]; Category)
-open import Categories.Category.BinaryProducts using (BinaryProducts)
 open import Categories.Category.Cartesian.Bundle using (CartesianCategory)
-open import Categories.Category.Cocartesian using (module CocartesianMonoidal; module CocartesianSymmetricMonoidal)
+open import Categories.Category.Cocartesian.Monoidal using (module CocartesianMonoidal)
+open import Categories.Category.Cocartesian.SymmetricMonoidal using (module CocartesianSymmetricMonoidal)
 open import Categories.Category.Monoidal.Symmetric using (Symmetric)
 open import Categories.Category.Monoidal.Braided using (Braided)
 open import Categories.Category.Monoidal.Core using (Monoidal)
@@ -27,7 +27,7 @@ open import Functor.Instance.Cospan.Stack 𝒞 using (⊗)
 open import Functor.Instance.Cospan.Embed 𝒞 using (L; L-resp-⊗)
 
 module 𝒞 = FinitelyCocompleteCategory 𝒞
-open CocartesianMonoidal 𝒞.U 𝒞.cocartesian using (⊥+--id; -+⊥-id; ⊥+A≅A; A+⊥≅A; +-monoidal)
+open CocartesianMonoidal 𝒞.cocartesian using (⊥+--id; -+⊥-id; ⊥+A≅A; A+⊥≅A; +-monoidal)
 open CocartesianSymmetricMonoidal 𝒞.U 𝒞.cocartesian using (+-symmetric)
 
 open Monoidal +-monoidal using () renaming (triangle to tri; pentagon to pent)
@@ -36,8 +36,7 @@ open import Categories.Category.Monoidal.Utilities +-monoidal using (associator-
 
 module _ where
 
-  open CartesianCategory FinitelyCocompletes-CC using (products)
-  open BinaryProducts products using (_×_)
+  open CartesianCategory FinitelyCocompletes-CC using (_×_)
 
   𝒞×𝒞 : FinitelyCocompleteCategory o ℓ e
   𝒞×𝒞 = 𝒞 × 𝒞
diff --git a/Category/Monoidal/Instance/DecoratedCospans/Products.agda b/Category/Monoidal/Instance/DecoratedCospans/Products.agda
index 647f887..4fd323e 100644
--- a/Category/Monoidal/Instance/DecoratedCospans/Products.agda
+++ b/Category/Monoidal/Instance/DecoratedCospans/Products.agda
@@ -21,7 +21,6 @@ import Categories.Morphism.Reasoning as ⇒-Reasoning
 
 open import Categories.Category using (_[_,_]; _[_≈_]; _[_∘_]; Category)
 open import Categories.Category.Core using (Category)
-open import Categories.Category.BinaryProducts using (BinaryProducts)
 open import Categories.Category.Cartesian using (Cartesian)
 open import Categories.Category.Cartesian.Bundle using (CartesianCategory)
 open import Categories.Functor using (Functor; _∘F_) renaming (id to idF)
@@ -44,8 +43,7 @@ module 𝒟 = SymmetricMonoidalCategory 𝒟
 
 module _ where
 
-  open CartesianCategory FinitelyCocompletes-CC using (products)
-  open BinaryProducts products using (_×_)
+  open CartesianCategory FinitelyCocompletes-CC using (_×_)
 
   𝒞×𝒞 : FinitelyCocompleteCategory o ℓ e
   𝒞×𝒞 = 𝒞 × 𝒞
@@ -57,8 +55,7 @@ module _ where
 
   module _ where
 
-    open Cartesian SymMonCat-Cartesian′ using (products)
-    open BinaryProducts products using (_×_; _⁂_)
+    open Cartesian SymMonCat-Cartesian′ using (_×_)
 
     𝒟×𝒟 : SymmetricMonoidalCategory o′ ℓ′ e′
     𝒟×𝒟 = 𝒟 × 𝒟
@@ -70,8 +67,7 @@ module _ where
 
   module _ where
 
-    open Cartesian SymMonCat-Cartesian using (products)
-    open BinaryProducts products using (_×_; _⁂_)
+    open Cartesian SymMonCat-Cartesian using (_×_)
 
     smc𝒞×𝒞 : SymmetricMonoidalCategory o ℓ e
     smc𝒞×𝒞 = smc 𝒞 × smc 𝒞
diff --git a/Category/Monoidal/Instance/Nat.agda b/Category/Monoidal/Instance/Nat.agda
index 24b30a6..23ee39d 100644
--- a/Category/Monoidal/Instance/Nat.agda
+++ b/Category/Monoidal/Instance/Nat.agda
@@ -6,7 +6,9 @@ open import Level using (0ℓ)
 open import Categories.Category.Monoidal.Bundle using (MonoidalCategory; SymmetricMonoidalCategory)
 open import Categories.Category.Instance.Nat using (Nat; Nat-Cartesian; Nat-Cocartesian; Natop)
 open import Categories.Category.Cartesian using (Cartesian)
-open import Categories.Category.Cocartesian using (Cocartesian; module CocartesianMonoidal; module CocartesianSymmetricMonoidal)
+open import Categories.Category.Cocartesian using (Cocartesian)
+open import Categories.Category.Cocartesian.Monoidal using (module CocartesianMonoidal)
+open import Categories.Category.Cocartesian.SymmetricMonoidal using (module CocartesianSymmetricMonoidal)
 open import Categories.Category.Cartesian.Monoidal using (module CartesianMonoidal)
 open import Categories.Category.Duality using (coCartesian⇒Cocartesian; Cocartesian⇒coCartesian)
 
@@ -26,7 +28,7 @@ module Monoidal where
 
   Nat,+,0 : MonoidalCategory 0ℓ 0ℓ 0ℓ
   Nat,+,0 .U = Nat
-  Nat,+,0 .monoidal = +-monoidal Nat Nat-Cocartesian
+  Nat,+,0 .monoidal = +-monoidal Nat-Cocartesian
 
   Nat,×,1 : MonoidalCategory 0ℓ 0ℓ 0ℓ
   Nat,×,1 .U = Nat
@@ -38,7 +40,7 @@ module Monoidal where
 
   Natop,×,1 : MonoidalCategory 0ℓ 0ℓ 0ℓ
   Natop,×,1 .U = Natop
-  Natop,×,1 .monoidal = +-monoidal Natop Natop-Cocartesian
+  Natop,×,1 .monoidal = +-monoidal Natop-Cocartesian
 
 module Symmetric where
 
@@ -50,7 +52,7 @@ module Symmetric where
 
   Nat,+,0 : SymmetricMonoidalCategory 0ℓ 0ℓ 0ℓ
   Nat,+,0 .U = Nat
-  Nat,+,0 .monoidal = +-monoidal Nat Nat-Cocartesian
+  Nat,+,0 .monoidal = +-monoidal Nat-Cocartesian
   Nat,+,0 .symmetric = +-symmetric Nat Nat-Cocartesian
 
   Nat,×,1 : SymmetricMonoidalCategory 0ℓ 0ℓ 0ℓ
@@ -65,7 +67,7 @@ module Symmetric where
 
   Natop,×,1 : SymmetricMonoidalCategory 0ℓ 0ℓ 0ℓ
   Natop,×,1 .U = Natop
-  Natop,×,1 .monoidal = +-monoidal Natop Natop-Cocartesian
+  Natop,×,1 .monoidal = +-monoidal Natop-Cocartesian
   Natop,×,1 .symmetric = +-symmetric Natop Natop-Cocartesian
 
 open Symmetric public