Use latest agda-categories

4 files changed, 27 insertions, 39 deletions

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)