Use latest agda-categories

23 files changed, 164 insertions, 201 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
diff --git a/Data/Matrix/SemiadditiveDagger.agda b/Data/Matrix/SemiadditiveDagger.agda
index ebc6592..1415c7e 100644
--- a/Data/Matrix/SemiadditiveDagger.agda
+++ b/Data/Matrix/SemiadditiveDagger.agda
@@ -286,15 +286,15 @@ coproduct {A} {B} = record
 
 opaque
   unfolding _≋_
-  !-unique : (E : Matrix 0 B) → []ᵥ ≋ E
-  !-unique E = ≋.reflexive (≡.sym ([]ᵥ-! E))
+  ¡-unique : (E : Matrix 0 B) → []ᵥ ≋ E
+  ¡-unique E = ≋.reflexive (≡.sym ([]ᵥ-! E))
 
 initial : Initial Mat
 initial = record
     { ⊥ = 0
     ; ⊥-is-initial = record
-        { ! = []ᵥ
-        ; !-unique = !-unique
+        { ¡ = []ᵥ
+        ; ¡-unique = ¡-unique
         }
     }
 
diff --git a/Functor/Cartesian/Instance/Underlying/SymmetricMonoidal/FinitelyCocomplete.agda b/Functor/Cartesian/Instance/Underlying/SymmetricMonoidal/FinitelyCocomplete.agda
index 346999b..537ac38 100644
--- a/Functor/Cartesian/Instance/Underlying/SymmetricMonoidal/FinitelyCocomplete.agda
+++ b/Functor/Cartesian/Instance/Underlying/SymmetricMonoidal/FinitelyCocomplete.agda
@@ -26,16 +26,8 @@ open import Category.Cocomplete.Finitely.Bundle using (FinitelyCocompleteCategor
 open import Category.Cartesian.Instance.SymMonCat {o} {ℓ} {e} using (SymMonCat-CC)
 open import Functor.Instance.Underlying.SymmetricMonoidal.FinitelyCocomplete {o} {ℓ} {e} using () renaming (Underlying to U)
 
-module CartesianCategory′ {o ℓ e : Level} (C : CartesianCategory o ℓ e) where
-  module CC = CartesianCategory C
-  open import Categories.Object.Terminal using (Terminal)
-  open Terminal CC.terminal public
-  open import Categories.Category.BinaryProducts using (BinaryProducts)
-  open BinaryProducts CC.products public
-  open CC public
-
-module FC = CartesianCategory′ FinitelyCocompletes-CC
-module SMC = CartesianCategory′ SymMonCat-CC
+module FC = CartesianCategory FinitelyCocompletes-CC
+module SMC = CartesianCategory SymMonCat-CC
 module U = Functor U
 
 F-resp-⊤ : IsTerminal SMC.U (U.₀ FC.⊤)
diff --git a/Functor/Exact/Instance/Swap.agda b/Functor/Exact/Instance/Swap.agda
index 99a27c5..98ca0f4 100644
--- a/Functor/Exact/Instance/Swap.agda
+++ b/Functor/Exact/Instance/Swap.agda
@@ -6,28 +6,26 @@ open import Category.Cocomplete.Finitely.Bundle using (FinitelyCocompleteCategor
 module Functor.Exact.Instance.Swap {o ℓ e : Level} (𝒞 𝒟 : FinitelyCocompleteCategory o ℓ e) where
 
 open import Categories.Category using (_[_,_])
-open import Categories.Category.BinaryProducts using (BinaryProducts)
 open import Categories.Category.Product using (Product) renaming (Swap to Swap′)
 open import Categories.Category.Cartesian using (Cartesian)
 open import Categories.Diagram.Coequalizer using (IsCoequalizer)
 open import Categories.Object.Initial using (IsInitial)
 open import Categories.Object.Coproduct using (IsCoproduct)
-open import Data.Product.Base using (_,_; proj₁; proj₂; swap)
+open import Data.Product using (_,_; proj₁; proj₂; swap)
 
 open import Category.Instance.FinitelyCocompletes {o} {ℓ} {e} using (FinitelyCocompletes-Cartesian)
 open import Functor.Exact using (RightExactFunctor)
 
 module FCC = Cartesian FinitelyCocompletes-Cartesian
-open BinaryProducts (FCC.products) using (_×_) -- ; π₁; π₂; _⁂_; assocˡ)
-
+open FCC using (_×_)
 
 module 𝒞 = FinitelyCocompleteCategory 𝒞
 module 𝒟 = FinitelyCocompleteCategory 𝒟
 
 swap-resp-⊥ : {A : 𝒞.Obj} {B : 𝒟.Obj} → IsInitial (Product 𝒞.U 𝒟.U) (A , B) → IsInitial (Product 𝒟.U 𝒞.U) (B , A)
 swap-resp-⊥ {A} {B} isInitial = record
-    { ! = swap !
-    ; !-unique = λ { (f , g) → swap (!-unique (g , f)) }
+    { ¡ = swap ¡
+    ; ¡-unique = λ { (f , g) → swap (¡-unique (g , f)) }
     }
   where
     open IsInitial isInitial
diff --git a/Functor/Instance/CMonoidalize.agda b/Functor/Instance/CMonoidalize.agda
index ad9b266..eef2bc8 100644
--- a/Functor/Instance/CMonoidalize.agda
+++ b/Functor/Instance/CMonoidalize.agda
@@ -12,7 +12,7 @@ module Functor.Instance.CMonoidalize
     (D : SymmetricMonoidalCategory o′ ℓ′ e′)
   where
 
-open import Categories.Category.Cocartesian using (module CocartesianSymmetricMonoidal)
+open import Categories.Category.Cocartesian.SymmetricMonoidal using (module CocartesianSymmetricMonoidal)
 open import Categories.Functor using (Functor)
 open import Category.Construction.CMonoids using (CMonoids)
 open import Categories.Category.Construction.Functors using (Functors)
diff --git a/Functor/Instance/Cospan/Stack.agda b/Functor/Instance/Cospan/Stack.agda
index b72219b..568b99d 100644
--- a/Functor/Instance/Cospan/Stack.agda
+++ b/Functor/Instance/Cospan/Stack.agda
@@ -43,8 +43,7 @@ id⊗id≈id {A} {B} = record
   where
     open Morphism U using (module ≅)
     open HomReasoning
-    open 𝒞 using (+-η; []-cong₂)
-    open coproduct {A} {B} using (i₁; i₂)
+    open 𝒞 using (i₁; i₂; +-η; []-cong₂)
     from∘f≈f : id ∘ [ i₁ ∘ id , i₂ ∘ id ] 𝒞.≈ id
     from∘f≈f = begin
         id ∘ [ i₁ ∘ id , i₂ ∘ id ]  ≈⟨ identityˡ ⟩
diff --git a/Functor/Instance/Decorate.agda b/Functor/Instance/Decorate.agda
index fedddba..8d5aefb 100644
--- a/Functor/Instance/Decorate.agda
+++ b/Functor/Instance/Decorate.agda
@@ -23,7 +23,8 @@ import Categories.Morphism.Reasoning as ⇒-Reasoning
 import Category.Diagram.Cospan 𝒞 as Cospan
 
 open import Categories.Category using (Category; _[_,_]; _[_≈_]; _[_∘_])
-open import Categories.Category.Cocartesian using (module CocartesianMonoidal)
+open import Categories.Category.Monoidal using (module Monoidal)
+open import Categories.Category.Cocartesian.Monoidal using (module CocartesianMonoidal)
 open import Categories.Category.Monoidal.Properties using (coherence-inv₃)
 open import Categories.Category.Monoidal.Utilities using (module Shorthands)
 open import Categories.Functor.Core using (Functor)
@@ -39,7 +40,7 @@ module 𝒟 = SymmetricMonoidalCategory 𝒟
 module F = SymmetricMonoidalFunctor F
 module Cospans = Category Cospans
 module DecoratedCospans = Category DecoratedCospans
-module mc𝒞 = CocartesianMonoidal 𝒞.U 𝒞.cocartesian
+module mc𝒞 = CocartesianMonoidal 𝒞.cocartesian
 
 -- For every cospan there exists a free decorated cospan
 -- i.e. the original cospan with the discrete decoration
@@ -90,7 +91,7 @@ homomorphism {g} {f} = record
 
     open DiagramPushout 𝒞.U using (Pushout)
     open Pushout (pushout f₂ g₁) using (i₁; i₂)
-    open mc𝒞 using (unitorˡ)
+    open Monoidal mc𝒞.+-monoidal using (unitorˡ)
     open unitorˡ using () renaming (to to λ⇐′)
 
     same-deco : F₁ 𝒞.id ∘ F₁ ¡ ∘ F.ε ≈ F₁ [ i₁ , i₂ ]′ ∘ φ (N , M) ∘ (F₁ ¡ ∘ ε) ⊗₁ (F₁ ¡ ∘ ε) ∘ ρ⇐
@@ -147,7 +148,7 @@ Decorate-resp-⊗ {f} {g} = record
     open F.⊗-homo using () renaming (η to φ; commute to φ-commute)
     open F using (F₁; ε)
     open Shorthands monoidal
-    open mc𝒞 using (unitorˡ)
+    open Monoidal mc𝒞.+-monoidal using (unitorˡ)
     open unitorˡ using () renaming (to to λ⇐′)
 
     same-deco : F₁ 𝒞.id ∘ F₁ ¡ ∘ ε ≈ φ (N , M) ∘ (F₁ ¡ ∘ ε) ⊗₁ (F₁ ¡ ∘ ε) ∘ ρ⇐
diff --git a/Functor/Instance/DecoratedCospan/Embed.agda b/Functor/Instance/DecoratedCospan/Embed.agda
index 77b16fa..15f3b57 100644
--- a/Functor/Instance/DecoratedCospan/Embed.agda
+++ b/Functor/Instance/DecoratedCospan/Embed.agda
@@ -32,7 +32,8 @@ import Categories.Diagram.Pushout as DiagramPushout
 import Categories.Diagram.Pushout.Properties as PushoutProperties
 import Categories.Morphism as Morphism
 
-open import Categories.Category.Cocartesian using (module CocartesianMonoidal)
+open import Categories.Category.Monoidal using (module Monoidal)
+open import Categories.Category.Cocartesian.Monoidal using (module CocartesianMonoidal)
 open import Categories.Category.Monoidal.Utilities using (module Shorthands)
 open import Categories.Functor using (Functor; _∘F_)
 open import Data.Product using (_,_)
@@ -44,7 +45,7 @@ module 𝒟 = SymmetricMonoidalCategory 𝒟
 module F = SymmetricMonoidalFunctor F
 module Cospans = Category Cospans
 module DecoratedCospans = Category DecoratedCospans
-module mc𝒞 = CocartesianMonoidal 𝒞.U 𝒞.cocartesian
+module mc𝒞 = CocartesianMonoidal 𝒞.cocartesian
 
 open import Functor.Instance.Decorate 𝒞 F using (Decorate; Decorate-resp-⊗)
 
@@ -74,7 +75,8 @@ module _ where
 
   module Codiagonal where
 
-    open mc𝒞 using (unitorˡ; unitorʳ; +-monoidal) public
+    open mc𝒞 using (+-monoidal) public
+    open Monoidal +-monoidal using (unitorˡ; unitorʳ) public
     open unitorˡ using () renaming (to to λ⇐′) public
     open unitorʳ using () renaming (to to ρ⇐′) public
     open 𝒞 using (U; _+_; []-cong₂; []∘+₁; ∘-distribˡ-[]; inject₁; inject₂; ¡)
@@ -122,7 +124,8 @@ module _ where
         open 𝒞 using (¡; ⊥; ¡-unique; pushout) renaming ([_,_] to [_,_]′; _+₁_ to infixr 10 _+₁_ )
         open 𝒞 using (U)
         open Category U
-        open mc𝒞 using (unitorˡ; unitorˡ-commute-to; +-monoidal) public
+        open mc𝒞 using (+-monoidal) public
+        open Monoidal +-monoidal using (unitorˡ; unitorˡ-commute-to) public
         open unitorˡ using () renaming (to to λ⇐′) public
         open ⊗-Reasoning +-monoidal
         open ⇒-Reasoning 𝒞.U
@@ -198,7 +201,8 @@ module _ where
         open 𝒞 using (¡; ⊥; ¡-unique; pushout) renaming ([_,_] to [_,_]′; _+₁_ to infixr 10 _+₁_ )
         open 𝒞 using (U)
         open Category U
-        open mc𝒞 using (unitorʳ; unitorˡ; unitorˡ-commute-to; +-monoidal) public
+        open mc𝒞 using (+-monoidal) public
+        open Monoidal +-monoidal using (unitorʳ; unitorˡ; unitorˡ-commute-to) public
         open unitorˡ using () renaming (to to λ⇐′) public
         open unitorʳ using () renaming (to to ρ⇐′) public
         open ⊗-Reasoning +-monoidal
diff --git a/Functor/Instance/DecoratedCospan/Stack.agda b/Functor/Instance/DecoratedCospan/Stack.agda
index 381ee06..e3eca81 100644
--- a/Functor/Instance/DecoratedCospan/Stack.agda
+++ b/Functor/Instance/DecoratedCospan/Stack.agda
@@ -23,16 +23,17 @@ import Categories.Category.Monoidal.Reasoning as ⊗-Reasoning
 import Functor.Instance.Cospan.Stack 𝒞 as Stack
 
 open import Categories.Category using (Category; _[_,_]; _[_≈_]; _[_∘_])
-open import Categories.Category.BinaryProducts using (BinaryProducts)
-open import Categories.Category.Monoidal.Utilities using (module Shorthands)
-open import Categories.Category.Monoidal.Properties using (coherence-inv₃)
+open import Categories.Category.Cocartesian.Monoidal using (module CocartesianMonoidal)
+open import Categories.Category.Cocartesian.SymmetricMonoidal using (module CocartesianSymmetricMonoidal)
+open import Categories.Category.Monoidal using (module Monoidal)
 open import Categories.Category.Monoidal.Braided.Properties using (braiding-coherence-inv)
+open import Categories.Category.Monoidal.Properties using (coherence-inv₃)
+open import Categories.Category.Monoidal.Utilities using (module Shorthands)
 open import Categories.Functor using (Functor)
 open import Categories.Functor.Bifunctor using (Bifunctor)
 open import Categories.Functor.Properties using ([_]-resp-≅)
-open import Categories.Category.Cocartesian using (module CocartesianMonoidal; module CocartesianSymmetricMonoidal)
-open import Categories.Object.Initial using (Initial)
 open import Categories.Object.Duality using (Coproduct⇒coProduct)
+open import Categories.Object.Initial using (Initial)
 open import Category.Instance.DecoratedCospans 𝒞 F using () renaming (DecoratedCospans to Cospans; _≈_ to _≈_′)
 
 import Category.Diagram.Cospan 𝒞 as Cospan
@@ -47,7 +48,7 @@ module Cospans = Category Cospans
 
 open 𝒞 using (Obj; _+_; cocartesian)
 
-module mc𝒞 = CocartesianMonoidal 𝒞.U cocartesian
+module mc𝒞 = CocartesianMonoidal cocartesian
 module smc𝒞 = CocartesianSymmetricMonoidal 𝒞.U cocartesian
 
 open DiagramPushout 𝒞.U using (Pushout)
@@ -73,9 +74,9 @@ id⊗id≈id {A} {B} = record
     ; same-deco = F.identity ⟩∘⟨refl
         ○ identityˡ
         ○ refl⟩∘⟨ ⊗-distrib-over-∘ ⟩∘⟨refl
-        ○ extendʳ (extendʳ (⊗-homo.commute (! , !)))
+        ○ extendʳ (extendʳ (⊗-homo.commute (¡ , ¡)))
         ○ refl⟩∘⟨ pullʳ (pushˡ serialize₂₁ ○ refl⟩∘⟨ sym unitorʳ-commute-to)
-        ○ pushˡ (F-resp-≈ !+!≈! ○ homomorphism)
+        ○ pushˡ (F-resp-≈ ¡+¡≈¡ ○ homomorphism)
         ○ refl⟩∘⟨ (refl⟩∘⟨ sym-assoc ○ pullˡ unitaryʳ ○ cancelˡ unitorʳ.isoʳ)
     }
   where
@@ -87,12 +88,12 @@ id⊗id≈id {A} {B} = record
     open ⊗-Reasoning monoidal
     open F using (module ⊗-homo; F-resp-≈; homomorphism; unitaryʳ)
     open 𝒞 using (initial)
-    open Initial initial using (!; !-unique₂)
+    open Initial initial using (¡; ¡-unique₂)
     open Morphism using (_≅_; module ≅)
     open mc𝒞 using (A+⊥≅A)
     module A+⊥≅A = _≅_ A+⊥≅A
-    !+!≈! : 𝒞.U [ (! {A} +₁ ! {B}) ≈ ! {A + B} 𝒞.∘ A+⊥≅A.from  ]
-    !+!≈! = 𝒞.Equiv.sym (flip-iso′ (≅.sym 𝒞.U A+⊥≅A) (¡-unique ((! +₁ !) 𝒞.∘ A+⊥≅A.to)))
+    ¡+¡≈¡ : 𝒞.U [ (¡ {A} +₁ ¡ {B}) ≈ ¡ {A + B} 𝒞.∘ A+⊥≅A.from  ]
+    ¡+¡≈¡ = 𝒞.Equiv.sym (flip-iso′ (≅.sym 𝒞.U A+⊥≅A) (¡-unique ((¡ +₁ ¡) 𝒞.∘ A+⊥≅A.to)))
 
 homomorphism
     : (A⇒B : Cospans [ A , B ])
@@ -148,12 +149,12 @@ homomorphism {A} {B} {C} {A′} {B′} {C′} f g f′ g′ = record
         open Shorthands mc𝒞.+-monoidal
         open ⊗-Reasoning mc𝒞.+-monoidal
         open ⇒-Reasoning U
-        open mc𝒞 using (assoc-commute-from; assoc-commute-to; module ⊗; associator)
+        open Monoidal mc𝒞.+-monoidal using (assoc-commute-from; assoc-commute-to; module ⊗; associator)
         open smc𝒞 using () renaming (module braiding to σ)
 
         module Codiagonal where
 
-          open 𝒞 using (coproduct; +-unique; []-cong₂; []∘+₁; ∘-distribˡ-[])
+          open 𝒞 using (coproduct; +-unique; []-cong₂; []∘+₁; ∘-distribˡ-[]; []∘+-assocʳ)
           μ : {X : Obj} → X + X ⇒ X
           μ = [ id , id ]′
 
@@ -163,16 +164,10 @@ homomorphism {A} {B} {C} {A′} {B′} {C′} f g f′ g′ = record
           μ∘σ : {X : Obj} → μ ∘ +-swap ≈ μ {X}
           μ∘σ = sym (+-unique (pullʳ inject₁ ○ inject₂) (pullʳ inject₂ ○ inject₁) )
 
-          op-binaryProducts : BinaryProducts op
-          op-binaryProducts = record { product = Coproduct⇒coProduct U coproduct }
-
-          module op-binaryProducts = BinaryProducts op-binaryProducts
-          open op-binaryProducts using () renaming (assocʳ∘⟨⟩ to []∘assocˡ)
-
           μ-assoc : {X : Obj} → μ {X} ∘ μ +₁ (id {X}) ≈ μ ∘ (id {X}) +₁ μ ∘ α⇒
           μ-assoc = begin
               μ ∘ μ +₁ id                   ≈⟨ μ∘+ ⟨
-              [ [ id , id ]′ , id ]′        ≈⟨ []∘assocˡ ⟨
+              [ [ id , id ]′ , id ]′        ≈⟨ []∘+-assocʳ ⟨
               [ id , [ id , id ]′ ]′ ∘ α⇒   ≈⟨ pushˡ μ∘+ ⟩
               μ ∘ id +₁ μ  ∘ α⇒             ∎
 
diff --git a/Functor/Instance/Monoidalize.agda b/Functor/Instance/Monoidalize.agda
index b856f82..b52c5fb 100644
--- a/Functor/Instance/Monoidalize.agda
+++ b/Functor/Instance/Monoidalize.agda
@@ -12,7 +12,7 @@ module Functor.Instance.Monoidalize
     (D : MonoidalCategory o′ ℓ′ e′)
   where
 
-open import Categories.Category.Cocartesian using (module CocartesianMonoidal)
+open import Categories.Category.Cocartesian.Monoidal using (module CocartesianMonoidal)
 
 open import Categories.Functor using (Functor)
 open import Categories.Functor.Monoidal using (MonoidalFunctor)
@@ -25,7 +25,7 @@ open import NaturalTransformation.Monoidal.Construction.MonoidValued cocartesian
 C-MC : MonoidalCategory o ℓ e
 C-MC = record { monoidal = +-monoidal }
   where
-    open CocartesianMonoidal C cocartesian
+    open CocartesianMonoidal cocartesian
 
 module C = MonoidalCategory C-MC
 module D = MonoidalCategory D
diff --git a/Functor/Instance/Underlying/SymmetricMonoidal/FinitelyCocomplete.agda b/Functor/Instance/Underlying/SymmetricMonoidal/FinitelyCocomplete.agda
index 8fabddd..456fe87 100644
--- a/Functor/Instance/Underlying/SymmetricMonoidal/FinitelyCocomplete.agda
+++ b/Functor/Instance/Underlying/SymmetricMonoidal/FinitelyCocomplete.agda
@@ -74,17 +74,17 @@ F₁ {A} {B} F = record
       open B.HomReasoning
       open B.Equiv
       open B using (_∘_; _≈_)
-      open B′ using (_+₁_; []-congˡ; []-congʳ; []-cong₂)
+      open B′ using (_+₁_; []-congˡ; []-congʳ; []-cong₂; ∘-distribˡ-[])
       open A′ using (_+_; i₁; i₂)
       ⊗-homo : NaturalTransformation (B.⊗ ∘F (F.F ⁂ F.F)) (F.F ∘F A.⊗)
       ⊗-homo = ntHelper record
           { η = λ { (X , Y) → +-iso.from {X} {Y} }
           ; commute = λ { {X , Y} {X′ , Y′} (f , g) →
-              B′.coproduct.∘-distribˡ-[]
-              ○ B′.coproduct.[]-cong₂
-                  (pullˡ B′.coproduct.inject₁ ○ [ F.F ]-resp-square (A.Equiv.sym A′.coproduct.inject₁))
-                  (pullˡ B′.coproduct.inject₂ ○ [ F.F ]-resp-square (A.Equiv.sym A′.coproduct.inject₂))
-              ○ sym B′.coproduct.∘-distribˡ-[] }
+              ∘-distribˡ-[]
+              ○ []-cong₂
+                  (pullˡ B′.inject₁ ○ [ F.F ]-resp-square (A.Equiv.sym A′.inject₁))
+                  (pullˡ B′.inject₂ ○ [ F.F ]-resp-square (A.Equiv.sym A′.inject₂))
+              ○ sym ∘-distribˡ-[] }
           }
       assoc
           : {X Y Z : A.Obj}
@@ -96,59 +96,59 @@ F₁ {A} {B} F = record
           ∘ B′.+-assocˡ
       assoc {X} {Y} {Z} = begin
           F.₁ A′.+-assocˡ ∘ +-iso.from ∘ (+-iso.from +₁ B.id)                               ≈⟨ refl⟩∘⟨ B′.[]∘+₁ ⟩
-          F.₁ A′.+-assocˡ ∘ B′.[ F.₁ i₁ ∘ +-iso.from , F.₁ i₂ ∘ B.id ]                      ≈⟨ refl⟩∘⟨ []-congʳ B′.coproduct.∘-distribˡ-[] ⟩
-          F.₁ A′.+-assocˡ ∘ B′.[ B′.[ F.₁ i₁ ∘ F.₁ i₁ , F.₁ i₁ ∘ F.₁ i₂ ] , F.₁ i₂ ∘ B.id ] ≈⟨ B′.coproduct.∘-distribˡ-[] ⟩
-          B′.[ F.₁ A′.+-assocˡ ∘ B′.[ F.₁ i₁ ∘ F.₁ i₁ , F.₁ i₁ ∘ F.₁ i₂ ] , _ ]             ≈⟨ []-congʳ B′.coproduct.∘-distribˡ-[] ⟩
-          B′.[ B′.[ F.₁ A′.+-assocˡ ∘ F.₁ i₁ ∘ F.₁ i₁ , F.₁ A′.+-assocˡ ∘ _ ] , _ ]         ≈⟨ []-congʳ ([]-congʳ (pullˡ ([ F.F ]-resp-∘ A′.coproduct.inject₁))) ⟩
-          B′.[ B′.[ F.₁ A′.[ i₁ , i₂ A′.∘ i₁ ] ∘ F.₁ i₁ , F.₁ A′.+-assocˡ ∘ _ ] , _ ]       ≈⟨ []-congʳ ([]-congʳ ([ F.F ]-resp-∘ A′.coproduct.inject₁)) ⟩
-          B′.[ B′.[ F.₁ i₁ , F.₁ A′.+-assocˡ ∘ F.₁ i₁ ∘ F.₁ i₂ ] , _ ]                      ≈⟨ []-congʳ ([]-congˡ (pullˡ ([ F.F ]-resp-∘ A′.coproduct.inject₁))) ⟩
-          B′.[ B′.[ F.₁ i₁ , F.₁ A′.[ i₁ , i₂ A′.∘ i₁ ] ∘ F.₁ i₂ ] , _ ]                    ≈⟨ []-congʳ ([]-congˡ ([ F.F ]-resp-∘ A′.coproduct.inject₂)) ⟩
-          B′.[ B′.[ F.₁ i₁ , F.₁ (i₂ A′.∘ i₁) ] , F.₁ A′.+-assocˡ ∘ F.₁ i₂ ∘ B.id ]         ≈⟨ []-congˡ (pullˡ ([ F.F ]-resp-∘ A′.coproduct.inject₂)) ⟩
+          F.₁ A′.+-assocˡ ∘ B′.[ F.₁ i₁ ∘ +-iso.from , F.₁ i₂ ∘ B.id ]                      ≈⟨ refl⟩∘⟨ []-congʳ ∘-distribˡ-[] ⟩
+          F.₁ A′.+-assocˡ ∘ B′.[ B′.[ F.₁ i₁ ∘ F.₁ i₁ , F.₁ i₁ ∘ F.₁ i₂ ] , F.₁ i₂ ∘ B.id ] ≈⟨ ∘-distribˡ-[] ⟩
+          B′.[ F.₁ A′.+-assocˡ ∘ B′.[ F.₁ i₁ ∘ F.₁ i₁ , F.₁ i₁ ∘ F.₁ i₂ ] , _ ]             ≈⟨ []-congʳ ∘-distribˡ-[] ⟩
+          B′.[ B′.[ F.₁ A′.+-assocˡ ∘ F.₁ i₁ ∘ F.₁ i₁ , F.₁ A′.+-assocˡ ∘ _ ] , _ ]         ≈⟨ []-congʳ ([]-congʳ (pullˡ ([ F.F ]-resp-∘ A′.inject₁))) ⟩
+          B′.[ B′.[ F.₁ A′.[ i₁ , i₂ A′.∘ i₁ ] ∘ F.₁ i₁ , F.₁ A′.+-assocˡ ∘ _ ] , _ ]       ≈⟨ []-congʳ ([]-congʳ ([ F.F ]-resp-∘ A′.inject₁)) ⟩
+          B′.[ B′.[ F.₁ i₁ , F.₁ A′.+-assocˡ ∘ F.₁ i₁ ∘ F.₁ i₂ ] , _ ]                      ≈⟨ []-congʳ ([]-congˡ (pullˡ ([ F.F ]-resp-∘ A′.inject₁))) ⟩
+          B′.[ B′.[ F.₁ i₁ , F.₁ A′.[ i₁ , i₂ A′.∘ i₁ ] ∘ F.₁ i₂ ] , _ ]                    ≈⟨ []-congʳ ([]-congˡ ([ F.F ]-resp-∘ A′.inject₂)) ⟩
+          B′.[ B′.[ F.₁ i₁ , F.₁ (i₂ A′.∘ i₁) ] , F.₁ A′.+-assocˡ ∘ F.₁ i₂ ∘ B.id ]         ≈⟨ []-congˡ (pullˡ ([ F.F ]-resp-∘ A′.inject₂)) ⟩
           B′.[ B′.[ F.₁ i₁ , F.₁ (i₂ A′.∘ i₁) ] , F.₁ (i₂ A′.∘ i₂) ∘ B.id ]                 ≈⟨ []-cong₂ ([]-congˡ F.homomorphism) (B.identityʳ ○ F.homomorphism) ⟩
-          B′.[ B′.[ F.₁ i₁ , F.₁ i₂ B′.∘ F.₁ i₁ ] , F.₁ i₂ ∘ F.₁ i₂ ]                       ≈⟨ []-congʳ ([]-congˡ B′.coproduct.inject₁) ⟨
-          B′.[ B′.[ F.₁ i₁ , B′.[ F.₁ i₂ B′.∘ F.₁ i₁  , _ ] ∘ B′.i₁ ] , _ ]                 ≈⟨ []-congʳ ([]-cong₂ (sym B′.coproduct.inject₁) (pushˡ (sym B′.coproduct.inject₂))) ⟩
-          B′.[ B′.[ B′.[ F.₁ i₁ , _ ] ∘ B′.i₁ , B′.[ F.₁ i₁ , _ ] ∘ B′.i₂ ∘ B′.i₁ ] , _ ]   ≈⟨ []-congʳ B′.coproduct.∘-distribˡ-[] ⟨
-          B′.[ B′.[ F.₁ i₁ , _ ] ∘ B′.[ B′.i₁ , B′.i₂ ∘ B′.i₁ ] , F.₁ i₂ ∘ F.₁ i₂ ]         ≈⟨ []-congˡ B′.coproduct.inject₂ ⟨
-          B′.[ B′.[ F.₁ i₁ , _ ] ∘ B′.[ _ , _ ] , B′.[ _ , F.₁ i₂ ∘ F.₁ i₂ ] ∘ B′.i₂ ]      ≈⟨ []-congˡ (pushˡ (sym B′.coproduct.inject₂)) ⟩
-          B′.[ B′.[ F.₁ i₁ , _ ] ∘ B′.[ _ , _ ] , B′.[ F.₁ i₁ , _ ] ∘ B′.i₂ ∘ B′.i₂ ]       ≈⟨ B′.coproduct.∘-distribˡ-[] ⟨
-          B′.[ F.₁ i₁ ,  B′.[ F.₁ i₂ ∘ F.₁ i₁ , F.₁ i₂ ∘ F.₁ i₂ ] ] ∘ B′.+-assocˡ           ≈⟨ []-cong₂ B.identityʳ (B′.coproduct.∘-distribˡ-[]) ⟩∘⟨refl ⟨
+          B′.[ B′.[ F.₁ i₁ , F.₁ i₂ B′.∘ F.₁ i₁ ] , F.₁ i₂ ∘ F.₁ i₂ ]                       ≈⟨ []-congʳ ([]-congˡ B′.inject₁) ⟨
+          B′.[ B′.[ F.₁ i₁ , B′.[ F.₁ i₂ B′.∘ F.₁ i₁  , _ ] ∘ B′.i₁ ] , _ ]                 ≈⟨ []-congʳ ([]-cong₂ (sym B′.inject₁) (pushˡ (sym B′.inject₂))) ⟩
+          B′.[ B′.[ B′.[ F.₁ i₁ , _ ] ∘ B′.i₁ , B′.[ F.₁ i₁ , _ ] ∘ B′.i₂ ∘ B′.i₁ ] , _ ]   ≈⟨ []-congʳ ∘-distribˡ-[] ⟨
+          B′.[ B′.[ F.₁ i₁ , _ ] ∘ B′.[ B′.i₁ , B′.i₂ ∘ B′.i₁ ] , F.₁ i₂ ∘ F.₁ i₂ ]         ≈⟨ []-congˡ B′.inject₂ ⟨
+          B′.[ B′.[ F.₁ i₁ , _ ] ∘ B′.[ _ , _ ] , B′.[ _ , F.₁ i₂ ∘ F.₁ i₂ ] ∘ B′.i₂ ]      ≈⟨ []-congˡ (pushˡ (sym B′.inject₂)) ⟩
+          B′.[ B′.[ F.₁ i₁ , _ ] ∘ B′.[ _ , _ ] , B′.[ F.₁ i₁ , _ ] ∘ B′.i₂ ∘ B′.i₂ ]       ≈⟨ ∘-distribˡ-[] ⟨
+          B′.[ F.₁ i₁ ,  B′.[ F.₁ i₂ ∘ F.₁ i₁ , F.₁ i₂ ∘ F.₁ i₂ ] ] ∘ B′.+-assocˡ           ≈⟨ []-cong₂ B.identityʳ (∘-distribˡ-[]) ⟩∘⟨refl ⟨
           B′.[ F.₁ i₁ B′.∘ B′.id , F.₁ i₂ ∘ B′.[ F.₁ i₁ , F.₁ i₂ ] ] ∘ B′.+-assocˡ          ≈⟨ pushˡ (sym B′.[]∘+₁) ⟩
           +-iso.from ∘ (B.id +₁ +-iso.from) ∘ B′.+-assocˡ                                   ∎
       unitaryˡ
           : {X : A.Obj}
-          → F.₁ A′.[ A′.initial.! , A.id {X} ]
+          → F.₁ A′.[ A′.¡ , A.id {X} ]
           ∘ B′.[ F.₁ i₁ , F.₁ i₂ ]
-          ∘ B′.[ B′.i₁ ∘ B′.initial.! , B′.i₂ ∘ B.id ]
-          ≈ B′.[ B′.initial.! , B.id ]
+          ∘ B′.[ B′.i₁ ∘ B′.¡ , B′.i₂ ∘ B.id ]
+          ≈ B′.[ B′.¡ , B.id ]
       unitaryˡ {X} = begin
-          F.₁ A′.[ A′.initial.! , A.id ] ∘ B′.[ F.₁ i₁ , F.₁ i₂ ] ∘ B′.[ _ , B′.i₂ ∘ B.id ]   ≈⟨ refl⟩∘⟨ B′.coproduct.∘-distribˡ-[] ⟩
-          _ ∘ B′.[ _ ∘ B′.i₁ ∘ B′.initial.! , B′.[ F.₁ i₁ , F.₁ i₂ ] ∘ B′.i₂ ∘ B.id ]         ≈⟨ refl⟩∘⟨ []-cong₂ (sym (B′.¡-unique _)) (pullˡ B′.coproduct.inject₂) ⟩
-          F.₁ A′.[ A′.initial.! , A.id ] ∘ B′.[ B′.initial.! , F.₁ i₂ ∘  B.id ]               ≈⟨ B′.coproduct.∘-distribˡ-[] ⟩
-          B′.[ _ ∘ B′.initial.! , F.₁ A′.[ A′.initial.! , A.id ] ∘ F.₁ i₂ ∘  B.id ]           ≈⟨ []-cong₂ (sym (B′.¡-unique _)) (pullˡ ([ F.F ]-resp-∘ A′.coproduct.inject₂)) ⟩
-          B′.[ B′.initial.! , F.₁ A.id ∘  B.id ]                                              ≈⟨ []-congˡ (elimˡ F.identity) ⟩
-          B′.[ B′.initial.! , B.id ]                                                          ∎
+          F.₁ A′.[ A′.¡ , A.id ] ∘ B′.[ F.₁ i₁ , F.₁ i₂ ] ∘ B′.[ _ , B′.i₂ ∘ B.id ]   ≈⟨ refl⟩∘⟨ ∘-distribˡ-[] ⟩
+          _ ∘ B′.[ _ ∘ B′.i₁ ∘ B′.¡ , B′.[ F.₁ i₁ , F.₁ i₂ ] ∘ B′.i₂ ∘ B.id ]         ≈⟨ refl⟩∘⟨ []-cong₂ (sym (B′.¡-unique _)) (pullˡ B′.inject₂) ⟩
+          F.₁ A′.[ A′.¡ , A.id ] ∘ B′.[ B′.¡ , F.₁ i₂ ∘  B.id ]                       ≈⟨ ∘-distribˡ-[] ⟩
+          B′.[ _ ∘ B′.¡ , F.₁ A′.[ A′.¡ , A.id ] ∘ F.₁ i₂ ∘  B.id ]                   ≈⟨ []-cong₂ (sym (B′.¡-unique _)) (pullˡ ([ F.F ]-resp-∘ A′.inject₂)) ⟩
+          B′.[ B′.¡ , F.₁ A.id ∘  B.id ]                                              ≈⟨ []-congˡ (elimˡ F.identity) ⟩
+          B′.[ B′.¡ , B.id ]                                                          ∎
       unitaryʳ
           : {X : A.Obj}
-          → F.₁ A′.[ A′.id {X} , A′.initial.! ]
+          → F.₁ A′.[ A′.id {X} , A′.¡ ]
           ∘ B′.[ F.₁ i₁ , F.₁ i₂ ]
-          ∘ B′.[ B′.i₁ ∘ B.id , B′.i₂ ∘ B′.initial.! ]
-          ≈ B′.[ B.id , B′.initial.! ]
+          ∘ B′.[ B′.i₁ ∘ B.id , B′.i₂ ∘ B′.¡ ]
+          ≈ B′.[ B.id , B′.¡ ]
       unitaryʳ {X} = begin
-          F.₁ A′.[ A.id , A′.initial.! ] ∘ B′.[ F.₁ i₁ , F.₁ i₂ ] ∘ B′.[ B′.i₁ ∘ B.id , _ ]   ≈⟨ refl⟩∘⟨ B′.coproduct.∘-distribˡ-[] ⟩
-          _ ∘ B′.[ B′.[ F.₁ i₁ , F.₁ i₂ ] ∘ B′.i₁ ∘ B.id , _ ∘ B′.i₂ ∘ B′.initial.! ]         ≈⟨ refl⟩∘⟨ []-cong₂ (pullˡ B′.coproduct.inject₁) (sym (B′.¡-unique _)) ⟩
-          F.₁ A′.[ A.id , A′.initial.! ] ∘ B′.[ F.₁ i₁ ∘  B.id , B′.initial.! ]               ≈⟨ B′.coproduct.∘-distribˡ-[] ⟩
-          B′.[ F.₁ A′.[ A.id , A′.initial.! ] ∘ F.₁ i₁ ∘  B.id , _ ∘ B′.initial.! ]           ≈⟨ []-cong₂ (pullˡ ([ F.F ]-resp-∘ A′.coproduct.inject₁)) (sym (B′.¡-unique _)) ⟩
-          B′.[ F.₁ A.id ∘  B.id , B′.initial.! ]                                              ≈⟨ []-congʳ (elimˡ F.identity) ⟩
-          B′.[ B.id , B′.initial.! ]                                                          ∎
+          F.₁ A′.[ A.id , A′.¡ ] ∘ B′.[ F.₁ i₁ , F.₁ i₂ ] ∘ B′.[ B′.i₁ ∘ B.id , _ ]   ≈⟨ refl⟩∘⟨ ∘-distribˡ-[] ⟩
+          _ ∘ B′.[ B′.[ F.₁ i₁ , F.₁ i₂ ] ∘ B′.i₁ ∘ B.id , _ ∘ B′.i₂ ∘ B′.¡ ]         ≈⟨ refl⟩∘⟨ []-cong₂ (pullˡ B′.inject₁) (sym (B′.¡-unique _)) ⟩
+          F.₁ A′.[ A.id , A′.¡ ] ∘ B′.[ F.₁ i₁ ∘  B.id , B′.¡ ]                       ≈⟨ ∘-distribˡ-[] ⟩
+          B′.[ F.₁ A′.[ A.id , A′.¡ ] ∘ F.₁ i₁ ∘  B.id , _ ∘ B′.¡ ]                   ≈⟨ []-cong₂ (pullˡ ([ F.F ]-resp-∘ A′.inject₁)) (sym (B′.¡-unique _)) ⟩
+          B′.[ F.₁ A.id ∘  B.id , B′.¡ ]                                              ≈⟨ []-congʳ (elimˡ F.identity) ⟩
+          B′.[ B.id , B′.¡ ]                                                          ∎
       braiding-compat
           : {X Y : A.Obj}
           → F.₁ A′.[ i₂ {X} {Y} , i₁ ] ∘ B′.[ F.₁ i₁ , F.₁ i₂ ]
           ≈ B′.[ F.F₁ i₁ , F.F₁ i₂ ] ∘ B′.[ B′.i₂ , B′.i₁ ]
       braiding-compat = begin
-          F.₁ A′.[ i₂ , i₁ ] ∘ B′.[ F.₁ i₁ , F.₁ i₂ ]                             ≈⟨ B′.coproduct.∘-distribˡ-[] ⟩
-          B′.[ F.₁ A′.[ i₂ , i₁ ] ∘ F.₁ i₁ , F.₁ A′.[ i₂ , i₁ ] ∘ F.₁ i₂ ]        ≈⟨ []-cong₂ ([ F.F ]-resp-∘ A′.coproduct.inject₁) ([ F.F ]-resp-∘ A′.coproduct.inject₂) ⟩
-          B′.[ F.₁ i₂ , F.₁ i₁ ]                                                  ≈⟨ []-cong₂ B′.coproduct.inject₂ B′.coproduct.inject₁ ⟨
-          B′.[ B′.[ F.₁ i₁ , F.₁ i₂ ] ∘ B′.i₂ , B′.[ F.₁ i₁ , F.₁ i₂ ] ∘ B′.i₁ ]  ≈⟨ B′.coproduct.∘-distribˡ-[] ⟨
+          F.₁ A′.[ i₂ , i₁ ] ∘ B′.[ F.₁ i₁ , F.₁ i₂ ]                             ≈⟨ ∘-distribˡ-[] ⟩
+          B′.[ F.₁ A′.[ i₂ , i₁ ] ∘ F.₁ i₁ , F.₁ A′.[ i₂ , i₁ ] ∘ F.₁ i₂ ]        ≈⟨ []-cong₂ ([ F.F ]-resp-∘ A′.inject₁) ([ F.F ]-resp-∘ A′.inject₂) ⟩
+          B′.[ F.₁ i₂ , F.₁ i₁ ]                                                  ≈⟨ []-cong₂ B′.inject₂ B′.inject₁ ⟨
+          B′.[ B′.[ F.₁ i₁ , F.₁ i₂ ] ∘ B′.i₂ , B′.[ F.₁ i₁ , F.₁ i₂ ] ∘ B′.i₁ ]  ≈⟨ ∘-distribˡ-[] ⟨
           B′.[ F.₁ i₁ , F.₁ i₂ ] ∘ B′.[ B′.i₂ , B′.i₁ ]   ∎
     open B-proofs
 
@@ -179,8 +179,8 @@ homomorphism {A} {B} {C} {F} {G} = record
             identityˡ
             ○ sym
                 ([]-cong₂
-                    ([ G.F ]-resp-∘ B.coproducts.inject₁)
-                    ([ G.F ]-resp-∘ B.coproducts.inject₂))
+                    ([ G.F ]-resp-∘ B.inject₁)
+                    ([ G.F ]-resp-∘ B.inject₂))
             ○ sym ∘-distribˡ-[]
             ○ pushʳ (introʳ C.⊗.identity)
         }
diff --git a/Functor/Monoidal/Construction/CMonoidValued.agda b/Functor/Monoidal/Construction/CMonoidValued.agda
index 2ac8be2..eb5c965 100644
--- a/Functor/Monoidal/Construction/CMonoidValued.agda
+++ b/Functor/Monoidal/Construction/CMonoidValued.agda
@@ -24,7 +24,7 @@ import Categories.Morphism.Reasoning as ⇒-Reasoning
 import Object.Monoid.Commutative as CommutativeMonoidObject
 import Functor.Monoidal.Construction.MonoidValued as MonoidValued
 
-open import Categories.Category.Cocartesian using (module CocartesianSymmetricMonoidal)
+open import Categories.Category.Cocartesian.SymmetricMonoidal using (module CocartesianSymmetricMonoidal)
 open import Categories.Category.Cocartesian.Bundle using (CocartesianCategory)
 open import Categories.Category.Construction.Monoids using (Monoids)
 open import Categories.Category.Monoidal.Symmetric.Properties using (module Shorthands)
diff --git a/Functor/Monoidal/Construction/MonoidValued.agda b/Functor/Monoidal/Construction/MonoidValued.agda
index 937714d..f8cd11f 100644
--- a/Functor/Monoidal/Construction/MonoidValued.agda
+++ b/Functor/Monoidal/Construction/MonoidValued.agda
@@ -26,7 +26,7 @@ import Categories.Morphism.Reasoning as ⇒-Reasoning
 import Categories.Object.Monoid as MonoidObject
 
 open import Categories.Category using (module Definitions)
-open import Categories.Category.Cocartesian using (module CocartesianMonoidal)
+open import Categories.Category.Cocartesian.Monoidal using (module CocartesianMonoidal)
 open import Categories.Category.Product using (_⁂_)
 open import Categories.Functor.Monoidal using (MonoidalFunctor; IsMonoidalFunctor)
 open import Categories.Functor.Properties using ([_]-resp-square; [_]-resp-∘)
@@ -41,7 +41,7 @@ private
   G = Forget ∙ M
 
   module 𝒞 = CocartesianCategory (record { cocartesian = 𝒞-+ })
-  module 𝒞-M = CocartesianMonoidal 𝒞 𝒞-+
+  module 𝒞-M = CocartesianMonoidal 𝒞-+
 
   𝒞-MC : MonoidalCategory o ℓ e
   𝒞-MC = record { monoidal = 𝒞-M.+-monoidal }