From a408cbee9abbe2dbeee09bd36afc678efe7b6557 Mon Sep 17 00:00:00 2001
From: Jacques Comeaux <jacquesrcomeaux@protonmail.com>
Date: Fri, 10 Jul 2026 17:21:14 -0700
Subject: Use latest agda-categories

---
 Category/Cocomplete/Finitely/Product.agda           | 20 +++++++++-----------
 Category/Cocomplete/Finitely/SymmetricMonoidal.agda |  4 ++--
 2 files changed, 11 insertions(+), 13 deletions(-)

(limited to 'Category/Cocomplete')

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
 
-- 
cgit v1.2.3