Use latest agda-categories

2 files changed, 24 insertions, 25 deletions

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 +₁ μ  ∘ α⇒             ∎