Use latest agda-categories

7 files changed, 78 insertions, 79 deletions

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)
         }