Use latest agda-categories

11 files changed, 73 insertions, 99 deletions

diff --git a/Category/Cartesian/Instance/FinitelyCocompletes.agda b/Category/Cartesian/Instance/FinitelyCocompletes.agda
index 8c779d5..c44388a 100644
--- a/Category/Cartesian/Instance/FinitelyCocompletes.agda
+++ b/Category/Cartesian/Instance/FinitelyCocompletes.agda
@@ -7,7 +7,6 @@ module Category.Cartesian.Instance.FinitelyCocompletes {o ℓ e : Level} where
 import Categories.Morphism as Morphism
 import Categories.Morphism.Reasoning as ⇒-Reasoning
 
-open import Categories.Category.BinaryProducts using (BinaryProducts)
 open import Categories.Category.Cartesian.Bundle using (CartesianCategory)
 open import Categories.Diagram.Coequalizer using (IsCoequalizer)
 open import Categories.Functor.Bifunctor using (flip-bifunctor)
@@ -30,7 +29,7 @@ FinitelyCocompletes-CC = record
     }
 
 module FinCoCom = CartesianCategory FinitelyCocompletes-CC
-open BinaryProducts (FinCoCom.products) using (_×_; π₁; π₂; _⁂_; assocˡ) --  hiding (unique)
+open FinCoCom using (_×_; π₁; π₂; assocˡ)
 
 module _ (𝒞 : FinitelyCocompleteCategory o ℓ e) where
 
@@ -49,8 +48,8 @@ module _ (𝒞 : FinitelyCocompleteCategory o ℓ e) where
       → IsInitial 𝒞×𝒞.U (A , B)
       → IsInitial 𝒞×𝒞.U (B , A)
   flip-IsInitial isInitial = let open IsInitial isInitial in record
-      { ! = swap !
-      ; !-unique = swap ∘′ !-unique ∘′ swap
+      { ¡ = swap ¡
+      ; ¡-unique = swap ∘′ ¡-unique ∘′ swap
       }
 
   flip-IsCoproduct
@@ -84,8 +83,8 @@ module _ (𝒞 : FinitelyCocompleteCategory o ℓ e) where
       → IsInitial 𝒞×𝒞.U (A , B)
       → IsInitial 𝒞.U (A + B)
   +-resp-⊥ {A , B} A,B-isInitial = record
-      { ! = [ A-isInitial.! , B-isInitial.! ]
-      ; !-unique = λ f → +-unique (sym (A-isInitial.!-unique (f ∘ i₁))) (sym (B-isInitial.!-unique (f ∘ i₂)))
+      { ¡ = [ A-isInitial.¡ , B-isInitial.¡ ]
+      ; ¡-unique = λ f → +-unique (sym (A-isInitial.¡-unique (f ∘ i₁))) (sym (B-isInitial.¡-unique (f ∘ i₂)))
       }
     where
       open IsRightExact
@@ -269,10 +268,6 @@ module _ {𝒞 : FinitelyCocompleteCategory o ℓ e} where
       module 𝒞×𝒞×𝒞 = FinitelyCocompleteCategory ((𝒞 × 𝒞) × 𝒞)
       open Morphism U using (_≅_; module ≅)
       module +-assoc {X} {Y} {Z} = _≅_ (≅.sym (+-assoc {X} {Y} {Z}))
-      open import Categories.Object.Duality 𝒞.U using (Coproduct⇒coProduct)
-      op-binaryProducts : BinaryProducts op
-      op-binaryProducts = record { product = Coproduct⇒coProduct coproduct }
-      open BinaryProducts op-binaryProducts using () renaming (assocʳ∘⁂ to +₁∘assocˡ)
       open Equiv
       commute
           : {((X , Y) , Z) : 𝒞×𝒞×𝒞.Obj}
@@ -280,4 +275,4 @@ module _ {𝒞 : FinitelyCocompleteCategory o ℓ e} where
           → (F : ((X , Y) , Z) 𝒞×𝒞×𝒞.⇒ ((X′ , Y′) , Z′))
           → (+-assoc.from 𝒞.∘ [x+y]+z.₁ F)
           ≈ (x+[y+z].₁ F 𝒞.∘ +-assoc.from)
-      commute {(X , Y) , Z} {(X′ , Y′) , Z′} ((F , G) , H) = sym +₁∘assocˡ
+      commute {(X , Y) , Z} {(X′ , Y′) , Z′} ((F , G) , H) = sym +₁∘+-assocʳ
diff --git a/Category/Cocomplete/Finitely/Product.agda b/Category/Cocomplete/Finitely/Product.agda
index 25dc346..4b74171 100644
--- a/Category/Cocomplete/Finitely/Product.agda
+++ b/Category/Cocomplete/Finitely/Product.agda
@@ -6,20 +6,21 @@ open import Level using (Level)
 module Category.Cocomplete.Finitely.Product {o ℓ e : Level} {𝒞 𝒟 : Category o ℓ e} where
 
 open import Categories.Category using (_[_,_])
+open import Categories.Category.BinaryCoproducts using (BinaryCoproducts)
+open import Categories.Category.Cocartesian using (Cocartesian)
 open import Categories.Category.Cocomplete.Finitely using (FinitelyCocomplete)
-open import Categories.Category.Cocartesian using (Cocartesian; BinaryCoproducts)
 open import Categories.Category.Product using (Product)
 open import Categories.Diagram.Coequalizer using (Coequalizer)
 open import Categories.Object.Coproduct using (Coproduct)
 open import Categories.Object.Initial using (IsInitial; Initial)
-open import Data.Product.Base using (_,_; _×_; dmap; zip; map)
+open import Data.Product using (_,_; _×_; dmap; zip; map)
 
 Initial-× : Initial 𝒞 → Initial 𝒟 → Initial (Product 𝒞 𝒟)
 Initial-× initial-𝒞 initial-𝒟 = record
     { ⊥ = 𝒞.⊥ , 𝒟.⊥
     ; ⊥-is-initial = record
-        { ! = 𝒞.! , 𝒟.!
-        ; !-unique = dmap 𝒞.!-unique 𝒟.!-unique
+        { ¡ = 𝒞.¡ , 𝒟.¡
+        ; ¡-unique = dmap 𝒞.¡-unique 𝒟.¡-unique
         }
     }
   where
@@ -31,20 +32,17 @@ Coproducts-× coproducts-𝒞 coproducts-𝒟 = record { coproduct = coproduct }
   where
     coproduct : ∀ {(A₁ , B₁) (A₂ , B₂) : _ × _} → Coproduct (Product 𝒞 𝒟) (A₁ , B₁) (A₂ , B₂)
     coproduct = record
-        { A+B = 𝒞.A+B , 𝒟.A+B
+        { A+B = _ 𝒞.+  _ , _ 𝒟.+ _
         ; i₁ = 𝒞.i₁ , 𝒟.i₁
         ; i₂ = 𝒞.i₂ , 𝒟.i₂
         ; [_,_] = zip 𝒞.[_,_] 𝒟.[_,_]
         ; inject₁ = 𝒞.inject₁ , 𝒟.inject₁
         ; inject₂ = 𝒞.inject₂ , 𝒟.inject₂
-        ; unique = zip 𝒞.unique 𝒟.unique
+        ; unique = zip 𝒞.+-unique 𝒟.+-unique
         }
       where
-        module Coprod {𝒞} (coprods : BinaryCoproducts 𝒞) where
-          open BinaryCoproducts coprods using (coproduct)
-          open coproduct public
-        module 𝒞 = Coprod coproducts-𝒞
-        module 𝒟 = Coprod coproducts-𝒟
+        module 𝒞 = BinaryCoproducts coproducts-𝒞
+        module 𝒟 = BinaryCoproducts coproducts-𝒟
 
 Coequalizer-×
     : (∀ {A} {B} (f g : 𝒞 [ A , B ]) → Coequalizer 𝒞 f g)
diff --git a/Category/Cocomplete/Finitely/SymmetricMonoidal.agda b/Category/Cocomplete/Finitely/SymmetricMonoidal.agda
index 2b66d19..bae9774 100644
--- a/Category/Cocomplete/Finitely/SymmetricMonoidal.agda
+++ b/Category/Cocomplete/Finitely/SymmetricMonoidal.agda
@@ -5,8 +5,8 @@ open import Categories.Category.Core using (Category)
 module Category.Cocomplete.Finitely.SymmetricMonoidal {o ℓ e} {𝒞 : Category o ℓ e} where
 
 open import Categories.Category.Cocomplete.Finitely 𝒞 using (FinitelyCocomplete)
-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)
 
 module FinitelyCocompleteSymmetricMonoidal (finCo : FinitelyCocomplete) where
 
diff --git a/Category/Dagger/Semiadditive.agda b/Category/Dagger/Semiadditive.agda
index 283f270..bf8c929 100644
--- a/Category/Dagger/Semiadditive.agda
+++ b/Category/Dagger/Semiadditive.agda
@@ -3,21 +3,20 @@
 open import Level using (Level; suc; _⊔_)
 open import Categories.Category using (Category)
 
-module Category.Dagger.Semiadditive
-    {o ℓ e : Level}
-    (𝒞 : Category o ℓ e)
-  where
+module Category.Dagger.Semiadditive {o ℓ e : Level} (𝒞 : Category o ℓ e) where
 
 import Categories.Category.Monoidal.Reasoning as ⊗-Reasoning
 import Categories.Morphism.Reasoning as ⇒-Reasoning
 
-open import Categories.Category.BinaryProducts using (BinaryProducts)
-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.Dagger using (HasDagger)
 open import Categories.Category.Monoidal using (Monoidal)
 open import Categories.Category.Monoidal.Symmetric using (module Symmetric)
 open import Categories.Category.Monoidal.Symmetric.Properties using () renaming (module Shorthands to σ-Shorthands)
 open import Categories.Category.Monoidal.Utilities using (module Shorthands)
+open import Categories.Functor using (Functor)
 open import Categories.Object.Duality using (Coproduct⇒coProduct)
 open import Relation.Binary using (Rel)
 
@@ -27,9 +26,9 @@ record DaggerCocartesianMonoidal : Set (suc (o ⊔ ℓ ⊔ e)) where
     cocartesian : Cocartesian
     dagger : HasDagger 𝒞
 
-  open Cocartesian cocartesian using (i₁; i₂)
-  open CocartesianMonoidal cocartesian using (+-monoidal; _⊗₀_; _⊗₁_)
-  open CocartesianSymmetricMonoidal cocartesian using (+-symmetric)
+  open Cocartesian cocartesian using (i₁; i₂) renaming (_+₁_ to _⊗₁_)
+  open CocartesianMonoidal cocartesian using (+-monoidal)
+  open CocartesianSymmetricMonoidal 𝒞 cocartesian using (+-symmetric)
   open HasDagger dagger using (_†; isUnitary; isSelfAdjoint)
   open Shorthands +-monoidal using (λ⇒; λ⇐; ρ⇒; ρ⇐; α⇒; α⇐)
   open σ-Shorthands +-symmetric using (σ⇒)
@@ -49,11 +48,11 @@ record SemiadditiveDagger : Set (suc (o ⊔ ℓ ⊔ e)) where
     daggerCocartesianMonoidal : DaggerCocartesianMonoidal
 
   open DaggerCocartesianMonoidal daggerCocartesianMonoidal public
-  open CocartesianMonoidal cocartesian using (+-monoidal) renaming (_⊗₀_ to _⊕₀_; _⊗₁_ to _⊕₁_; ⊗ to ⊕) public
-
+  open Cocartesian cocartesian using ([]∘+-assocʳ; []∘+-swap) renaming (_+_ to _⊕₀_; _+₁_ to infixr 10 _⊕₁_; -+- to ⊕) public
+  open CocartesianMonoidal cocartesian using (+-monoidal) public
   open Cocartesian cocartesian using (i₁; i₂; ¡) public
   open Cocartesian cocartesian using (⊥; [_,_]; ∘[]; []∘+₁; []-cong₂; coproduct; ¡-unique; inject₁; inject₂; +-unique; +-g-η)
-  open CocartesianSymmetricMonoidal cocartesian using (+-symmetric)
+  open CocartesianSymmetricMonoidal 𝒞 cocartesian using (+-symmetric)
   open HasDagger dagger using (_†; †-involutive; ⟨_⟩†; †-identity; †-homomorphism) public
   open Monoidal +-monoidal using (unitorˡ-commute-from; unitorʳ-commute-from; assoc-commute-from; module unitorˡ; module unitorʳ; module associator)
   open σ-Shorthands +-symmetric using (σ⇒)
@@ -61,6 +60,8 @@ record SemiadditiveDagger : Set (suc (o ⊔ ℓ ⊔ e)) where
   open Shorthands +-monoidal using (λ⇒; λ⇐; ρ⇒; ρ⇐; α⇒; α⇐)
   open Category 𝒞
 
+  module ⊕ = Functor ⊕
+
   -- projection maps
   p₁ : {A B : Obj} → A ⊕₀ B ⇒ A
   p₁ = i₁ †
@@ -76,11 +77,6 @@ record SemiadditiveDagger : Set (suc (o ⊔ ℓ ⊔ e)) where
   △ : {A : Obj} → A ⇒ A ⊕₀ A
   △ = ▽ †
 
-  private
-    op-binaryProducts : BinaryProducts op
-    op-binaryProducts = record { product = Coproduct⇒coProduct 𝒞 coproduct }
-    open BinaryProducts op-binaryProducts using () renaming (assocʳ∘⟨⟩ to []-assoc; swap∘⟨⟩ to []∘swap)
-
   open ⊗-Reasoning +-monoidal
   open ⇒-Reasoning 𝒞
 
@@ -88,7 +84,7 @@ record SemiadditiveDagger : Set (suc (o ⊔ ℓ ⊔ e)) where
   ▽-assoc = begin
       [ id , id ] ∘ [ id , id ] ⊕₁ id       ≈⟨ []∘+₁ ⟩
       [ id ∘ [ id , id ] , id ∘ id ]        ≈⟨ []-cong₂ identityˡ identityˡ ⟩
-      [ [ id , id ] , id ]                  ≈⟨ []-assoc ⟨
+      [ [ id , id ] , id ]                  ≈⟨ []∘+-assocʳ ⟨
       [ id , [ id , id ] ] ∘ α⇒             ≈⟨ []-cong₂ identityˡ identityˡ ⟩∘⟨refl ⟨
       [ id ∘ id , id ∘ [ id , id ] ] ∘ α⇒   ≈⟨ pushˡ (Equiv.sym []∘+₁) ⟩
       [ id , id ] ∘ id ⊕₁ [ id , id ] ∘ α⇒  ∎
@@ -144,7 +140,7 @@ record SemiadditiveDagger : Set (suc (o ⊔ ℓ ⊔ e)) where
       ρ⇐                    ∎
 
   ▽-comm : {A : Obj} → ▽ {A} ∘ σ⇒ ≈ ▽
-  ▽-comm = []∘swap
+  ▽-comm = []∘+-swap
 
   △-comm : {A : Obj} → σ⇒ ∘ △ {A} ≈ △
   △-comm = begin
diff --git a/Category/Instance/DecoratedCospans.agda b/Category/Instance/DecoratedCospans.agda
index b527265..480803e 100644
--- a/Category/Instance/DecoratedCospans.agda
+++ b/Category/Instance/DecoratedCospans.agda
@@ -23,7 +23,7 @@ import Category.Instance.Cospans 𝒞 as Cospans
 import Category.Diagram.Cospan 𝒞 as Cospan
 
 open import Categories.Category using (Category; _[_∘_])
-open import Categories.Category.Cocartesian using (module CocartesianMonoidal)
+open import Categories.Category.Cocartesian.Monoidal using (module CocartesianMonoidal)
 open import Categories.Diagram.Pushout using (Pushout)
 open import Categories.Diagram.Pushout.Properties 𝒞.U using (up-to-iso)
 open import Categories.Functor.Properties using ([_]-resp-≅; [_]-resp-square)
@@ -71,7 +71,7 @@ compose c₁ c₂ = record
 identity : DecoratedCospan A A
 identity = record
     { cospan = Cospan.identity
-    ; decoration = 𝒟.U [ F₁ 𝒞.initial.! ∘ ε ]
+    ; decoration = 𝒟.U [ F₁ 𝒞.¡ ∘ ε ]
     }
 
 record _≈_ (C₁ C₂ : DecoratedCospan A B) : Set (ℓ ⊔ e ⊔ e′) where
@@ -222,10 +222,7 @@ compose-assoc {A} {B} {C} {D} {c₁} {c₂} {c₃} = record
 
     module _ where
 
-      open 𝒞 using (∘[]; []-congʳ; []-congˡ; []∘+₁)
-      open 𝒞.Dual.op-binaryProducts 𝒞.cocartesian
-          using ()
-          renaming (⟨⟩-cong₂ to []-cong₂; assocˡ∘⟨⟩ to []∘assocˡ)
+      open 𝒞 using (∘[]; []-congʳ; []-congˡ; []∘+₁; []∘+-assocˡ; []-cong₂)
 
       open ⇒-Reasoning 𝒞.U
       open 𝒞 using (id; _∘_; _≈_; assoc; identityʳ)
@@ -241,7 +238,7 @@ compose-assoc {A} {B} {C} {D} {c₁} {c₂} {c₃} = record
           [ (y ∘ f) ∘ id , (l ∘ k) ∘ [ h , i ] ]            ≈⟨ []-cong₂ identityʳ ∘[] ⟩
           [ y ∘ f , [ (l ∘ k) ∘ h , (l ∘ k) ∘ i ] ]         ≈⟨ []-congˡ ([]-cong₂ (pullʳ (sym P₃.commute)) (assoc ○ P₂₃.universal∘i₂≈h₂)) ⟩
           [ y ∘ f , [ l ∘ j ∘ g , z ] ]                     ≈⟨ []-congˡ ([]-congʳ (pullˡ P₂₃.universal∘i₁≈h₁)) ⟩
-          [ y ∘ f , [ y ∘ g , z ] ]                         ≈⟨ []∘assocˡ ⟨
+          [ y ∘ f , [ y ∘ g , z ] ]                         ≈⟨ []∘+-assocˡ ⟨
           [ [ y ∘ f , y ∘ g ] , z ] ∘ +-assoc.from          ≈⟨ []-cong₂ ∘[] identityʳ ⟩∘⟨refl ⟨
           [ y ∘ [ f ,  g ] , z ∘ id ] ∘ +-assoc.from        ≈⟨ pullˡ []∘+₁ ⟨
           [ y , z ] ∘ ([ f , g ] +₁ id) ∘ +-assoc.from      ∎
@@ -404,7 +401,7 @@ compose-idʳ {A} {_} {C} = record
     open 𝒞
       using (cocartesian)
       renaming (id to id′; _∘_ to _∘′_)
-    open CocartesianMonoidal 𝒞.U cocartesian using (⊥+A≅A)
+    open CocartesianMonoidal cocartesian using (⊥+A≅A)
     module ⊥+A≅A {a} = _≅_ (⊥+A≅A {a})
     module _ where
       open 𝒞
@@ -412,13 +409,10 @@ compose-idʳ {A} {_} {C} = record
           ( _⇒_ ; _∘_ ; _≈_ ; id ; U
           ; identity²
           ; cocartesian ; initial ; ¡-unique
-          ; ∘[] ; []∘+₁ ; inject₂ ; assoc
-          ; module HomReasoning ; module Dual ; module Equiv
+          ; ∘[] ; []∘+₁ ; inject₂ ; assoc ; []-cong₂
+          ; module HomReasoning ; module Equiv
           )
       open Equiv
-      open Dual.op-binaryProducts cocartesian
-        using ()
-        renaming (⟨⟩-cong₂ to []-cong₂)
       open ⇒-Reasoning U
       open HomReasoning
       copairing-id : ((≅P.from ∘ [ i₁ , i₂ ]) ∘ (¡ +₁ id)) ∘ ⊥+A≅A.to 𝒞.≈ id
@@ -502,7 +496,7 @@ compose-idˡ {_} {B} {C} = record
       using (cocartesian)
       renaming (id to id′; _∘_ to _∘′_)
 
-    open CocartesianMonoidal 𝒞.U cocartesian using (A+⊥≅A)
+    open CocartesianMonoidal cocartesian using (A+⊥≅A)
 
     module A+⊥≅A {a} = _≅_ (A+⊥≅A {a})
 
@@ -513,16 +507,12 @@ compose-idˡ {_} {B} {C} = record
           ( _⇒_ ; _∘_ ; _≈_ ; id ; U
           ; identity²
           ; cocartesian ; initial ; ¡-unique
-          ; ∘[] ; []∘+₁ ; inject₁ ; assoc
-          ; module HomReasoning ; module Dual ; module Equiv
+          ; ∘[] ; []∘+₁ ; inject₁ ; assoc ; []-cong₂
+          ; module HomReasoning ; module Equiv
           )
 
       open Equiv
 
-      open Dual.op-binaryProducts cocartesian
-        using ()
-        renaming (⟨⟩-cong₂ to []-cong₂)
-
       open ⇒-Reasoning U
       open HomReasoning
 
@@ -652,11 +642,7 @@ compose-equiv {_} {_} {_} {c₂} {c₂′} {c₁} {c₁′} ≅C₂ ≅C₁ = re
       open ⊗-Util 𝒟.monoidal using (module Shorthands)
       open Shorthands using (ρ⇒; ρ⇐)
 
-      open 𝒞 using ([_,_]; ∘[]; _+_; _+₁_; []∘+₁) renaming (_∘_ to _∘′_)
-      open 𝒞.Dual.op-binaryProducts 𝒞.cocartesian
-          using ()
-          renaming (⟨⟩-cong₂ to []-cong₂)
-
+      open 𝒞 using ([_,_]; ∘[]; _+_; _+₁_; []∘+₁; []-cong₂) renaming (_∘_ to _∘′_)
       open 𝒟
 
       φ[N,M] : F₀ N ⊗₀ F₀ M 𝒟.⇒ F₀ (N + M)
diff --git a/Category/Instance/FinitelyCocompletes.agda b/Category/Instance/FinitelyCocompletes.agda
index 9bee58e..ceb1d53 100644
--- a/Category/Instance/FinitelyCocompletes.agda
+++ b/Category/Instance/FinitelyCocompletes.agda
@@ -84,8 +84,8 @@ module _ (𝒞 𝒟 : FinitelyCocompleteCategory o ℓ e) where
           → IsInitial 𝒞×𝒟.U (A , B)
           → IsInitial 𝒞.U A
       F-resp-⊥ {A , B} initial = record
-          { ! = λ { {C} → proj₁ (! {C , B}) }
-          ; !-unique = λ { f → proj₁ (!-unique (f , 𝒟.id)) }
+          { ¡ = λ { {C} → proj₁ (¡ {C , B}) }
+          ; ¡-unique = λ { f → proj₁ (¡-unique (f , 𝒟.id)) }
           }
         where
           open IsInitial initial
@@ -130,8 +130,8 @@ module _ (𝒞 𝒟 : FinitelyCocompleteCategory o ℓ e) where
           → IsInitial 𝒞×𝒟.U (A , B)
           → IsInitial 𝒟.U B
       F-resp-⊥ {A , B} initial = record
-          { ! = λ { {C} → proj₂ (! {A , C}) }
-          ; !-unique = λ { f → proj₂ (!-unique (𝒞.id , f)) }
+          { ¡ = λ { {C} → proj₂ (¡ {A , C}) }
+          ; ¡-unique = λ { f → proj₂ (¡-unique (𝒞.id , f)) }
           }
         where
           open IsInitial initial
@@ -193,8 +193,8 @@ module _ where
           → IsInitial 𝒞.U A
           → IsInitial (ProductCat 𝒟.U ℰ.U) (F.₀ A , G.₀ A)
       F-resp-⊥′ A-isInitial = record
-          { ! = F[A]-isInitial.! , G[A]-isInitial.!
-          ; !-unique = dmap F[A]-isInitial.!-unique G[A]-isInitial.!-unique
+          { ¡ = F[A]-isInitial.¡ , G[A]-isInitial.¡
+          ; ¡-unique = dmap F[A]-isInitial.¡-unique G[A]-isInitial.¡-unique
           }
         where
           module F[A]-isInitial = IsInitial (F-resp-⊥ A-isInitial)
@@ -254,20 +254,20 @@ module _ where
           → IsInitial 𝒜×ℬ.U (A , B)
           → IsInitial 𝒞×𝒟.U (F.₀ A , G.₀ B)
       F-resp-⊥′ {A , B} A,B-isInitial = record
-          { ! = F[A]-isInitial.! , G[B]-isInitial.!
-          ; !-unique = dmap F[A]-isInitial.!-unique G[B]-isInitial.!-unique
+          { ¡ = F[A]-isInitial.¡ , G[B]-isInitial.¡
+          ; ¡-unique = dmap F[A]-isInitial.¡-unique G[B]-isInitial.¡-unique
           }
         where
           module A,B-isInitial = IsInitial A,B-isInitial
           A-isInitial : IsInitial 𝒜.U A
           A-isInitial = record
-              { ! = λ { {X} → proj₁ (A,B-isInitial.! {X , B}) }
-              ; !-unique = λ { f → proj₁ (A,B-isInitial.!-unique (f , ℬ.id)) }
+              { ¡ = λ { {X} → proj₁ (A,B-isInitial.¡ {X , B}) }
+              ; ¡-unique = λ { f → proj₁ (A,B-isInitial.¡-unique (f , ℬ.id)) }
               }
           B-isInitial : IsInitial ℬ.U B
           B-isInitial = record
-              { ! = λ { {X} → proj₂ (A,B-isInitial.! {A , X}) }
-              ; !-unique = λ { f → proj₂ (A,B-isInitial.!-unique (𝒜.id , f)) }
+              { ¡ = λ { {X} → proj₂ (A,B-isInitial.¡ {A , X}) }
+              ; ¡-unique = λ { f → proj₂ (A,B-isInitial.¡-unique (𝒜.id , f)) }
               }
           module F[A]-isInitial = IsInitial (F-resp-⊥ A-isInitial)
           module G[B]-isInitial = IsInitial (G-resp-⊥ B-isInitial)
diff --git a/Category/Instance/One/Properties.agda b/Category/Instance/One/Properties.agda
index c6261bb..2d75139 100644
--- a/Category/Instance/One/Properties.agda
+++ b/Category/Instance/One/Properties.agda
@@ -13,7 +13,7 @@ One = One′ {o} {ℓ} {e}
 open import Categories.Category.Cocartesian One using (Cocartesian)
 open import Categories.Category.Cocomplete.Finitely One using (FinitelyCocomplete)
 open import Categories.Object.Initial One using (Initial)
-open import Categories.Category.Cocartesian One using (BinaryCoproducts)
+open import Categories.Category.BinaryCoproducts One using (BinaryCoproducts)
 
 
 initial : Initial
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)
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