From b65266b7b41e3001eb3cf46c95ee6c9af021edc9 Mon Sep 17 00:00:00 2001
From: Jacques Comeaux <jacquesrcomeaux@protonmail.com>
Date: Thu, 30 Jul 2026 15:47:52 -0700
Subject: Update missed module to new agda-categories

---
 Category/Monoidal/Instance/DecoratedCospans.agda | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

(limited to 'Category/Monoidal')

diff --git a/Category/Monoidal/Instance/DecoratedCospans.agda b/Category/Monoidal/Instance/DecoratedCospans.agda
index b0625ab..8cd2e94 100644
--- a/Category/Monoidal/Instance/DecoratedCospans.agda
+++ b/Category/Monoidal/Instance/DecoratedCospans.agda
@@ -26,10 +26,10 @@ import Categories.Category.Monoidal.Properties as ⊗-Properties
 import Categories.Category.Monoidal.Braided.Properties as σ-Properties
 
 open import Categories.Category 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.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.Braided using (Braided)
 open import Categories.Category.Monoidal.Core using (Monoidal)
 open import Categories.Category.Monoidal.Symmetric using (Symmetric)
@@ -51,7 +51,7 @@ open import Functor.Instance.DecoratedCospan.Stack 𝒞 F using (⊗)
 open import Functor.Instance.DecoratedCospan.Embed 𝒞 F using (L; L-resp-⊗; B₁)
 
 open import Category.Monoidal.Instance.DecoratedCospans.Products 𝒞 F
-open CocartesianMonoidal 𝒞.U 𝒞.cocartesian using (⊥+--id; -+⊥-id; ⊥+A≅A; A+⊥≅A; +-monoidal)
+open CocartesianMonoidal 𝒞.cocartesian using (⊥+--id; -+⊥-id; ⊥+A≅A; A+⊥≅A; +-monoidal)
 open import Categories.Category.Monoidal.Utilities +-monoidal using (associator-naturalIsomorphism)
 
 module LiftUnitorˡ where
@@ -61,7 +61,7 @@ module LiftUnitorˡ where
     ≃₁ : NaturalTransformation (Hom[ 𝒟.U ][ 𝒟.unit ,-] ∘F F.F) (Hom[ 𝒟.U ][ 𝒟.unit ,-] ∘F F.F ∘F (⊥ +-))
     ≃₁ = ntHelper record
         { η = λ { X → record
-            { to = λ { f → 𝒟.U [ F.⊗-homo.η (⊥ , X) ∘ 𝒟.U [ 𝒟.⊗.₁ (𝒟.U [ F.₁ 𝒞.initial.! ∘ F.ε ] , f) ∘ ρ⇐ ] ] }
+            { to = λ { f → 𝒟.U [ F.⊗-homo.η (⊥ , X) ∘ 𝒟.U [ 𝒟.⊗.₁ (𝒟.U [ F.₁ 𝒞.¡ ∘ F.ε ] , f) ∘ ρ⇐ ] ] }
             ; cong = λ { x → refl⟩∘⟨ refl⟩⊗⟨ x ⟩∘⟨refl } }
             }
         ; commute = ned
@@ -105,7 +105,7 @@ module LiftUnitorˡ where
         F.⊗-homo.η (⊥ , X) ∘ (F.₁ ¡ ∘ F.ε) ⊗₁ f ∘ ρ⇐                    ∎
       where
         open Shorthands 𝒞.monoidal using (λ⇐)
-        open CocartesianMonoidal 𝒞.U 𝒞.cocartesian using (unitorˡ)
+        open Monoidal +-monoidal using (unitorˡ)
         open 𝒟.Equiv
         open 𝒟 using (sym-assoc; _∘_; id; _⊗₁_; identityʳ)
         open ⊗-Reasoning 𝒟.monoidal
@@ -122,7 +122,7 @@ module LiftUnitorʳ where
     ≃₁ : NaturalTransformation (Hom[ 𝒟.U ][ 𝒟.unit ,-] ∘F F.F) (Hom[ 𝒟.U ][ 𝒟.unit ,-] ∘F F.F ∘F (-+ ⊥))
     ≃₁ = ntHelper record
         { η = λ { X → record
-            { to = λ { f → 𝒟.U [ F.⊗-homo.η (X , ⊥) ∘ 𝒟.U [ 𝒟.⊗.₁ (f , 𝒟.U [ F.₁ 𝒞.initial.! ∘ F.ε ]) ∘ ρ⇐ ] ] }
+            { to = λ { f → 𝒟.U [ F.⊗-homo.η (X , ⊥) ∘ 𝒟.U [ 𝒟.⊗.₁ (f , 𝒟.U [ F.₁ 𝒞.¡ ∘ F.ε ]) ∘ ρ⇐ ] ] }
             ; cong = λ { x → refl⟩∘⟨ x ⟩⊗⟨refl ⟩∘⟨refl } }
             }
         ; commute = ned
@@ -165,7 +165,7 @@ module LiftUnitorʳ where
         F.⊗-homo.η (X , ⊥) ∘ f ⊗₁ (F.₁ ¡ ∘ F.ε) ∘ ρ⇐                    ∎
       where
         open Shorthands 𝒞.monoidal using () renaming (ρ⇐ to ρ⇐′)
-        open CocartesianMonoidal 𝒞.U 𝒞.cocartesian using (unitorʳ)
+        open Monoidal +-monoidal using (unitorʳ)
         open 𝒟.Equiv
         open 𝒟 using (sym-assoc; _∘_; id; _⊗₁_; identityʳ)
         open ⊗-Reasoning 𝒟.monoidal
@@ -279,7 +279,7 @@ module LiftAssociator where
         open 𝒟 using (sym-assoc; _∘_; id; _⊗₁_; identityʳ; assoc-commute-from; unitorˡ-commute-to) renaming (unitorˡ to ƛ; associator to α)
         open ⊗-Reasoning 𝒟.monoidal
         open ⇒-Reasoning 𝒟.U
-        open CocartesianMonoidal 𝒞.U 𝒞.cocartesian using () renaming (associator to α′)
+        open Monoidal +-monoidal using () renaming (associator to α′)
         open ⊗-Properties 𝒟.monoidal using (coherence-inv₁; coherence-inv₃)
     module Associator = Square {[𝒞×𝒞]×𝒞} {𝒞} {[𝒟×𝒟]×𝒟} {𝒟} {[F×F]×F} {F} {[x+y]+z.F {𝒞}} {x+[y+z].F {𝒞}} (assoc-≃ {𝒞}) ≃₁ ≃₂ ≃₂≋≃₁
 open LiftAssociator using (module Associator)
-- 
cgit v1.2.3