From a408cbee9abbe2dbeee09bd36afc678efe7b6557 Mon Sep 17 00:00:00 2001 From: Jacques Comeaux Date: Fri, 10 Jul 2026 17:21:14 -0700 Subject: Use latest agda-categories --- Category/Monoidal/Instance/Cospans.agda | 9 ++++----- Category/Monoidal/Instance/DecoratedCospans/Products.agda | 10 +++------- Category/Monoidal/Instance/Nat.agda | 12 +++++++----- 3 files changed, 14 insertions(+), 17 deletions(-) (limited to 'Category/Monoidal') diff --git a/Category/Monoidal/Instance/Cospans.agda b/Category/Monoidal/Instance/Cospans.agda index a1648db..187eaca 100644 --- a/Category/Monoidal/Instance/Cospans.agda +++ b/Category/Monoidal/Instance/Cospans.agda @@ -9,9 +9,9 @@ import Categories.Morphism as Morphism import Categories.Morphism.Reasoning.Iso as IsoReasoning open import Categories.Category using (_[_,_]; _[_β‰ˆ_]; _[_∘_]; Category) -open import Categories.Category.BinaryProducts using (BinaryProducts) 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.Symmetric using (Symmetric) open import Categories.Category.Monoidal.Braided using (Braided) open import Categories.Category.Monoidal.Core using (Monoidal) @@ -27,7 +27,7 @@ open import Functor.Instance.Cospan.Stack π’ž using (βŠ—) open import Functor.Instance.Cospan.Embed π’ž using (L; L-resp-βŠ—) module π’ž = FinitelyCocompleteCategory π’ž -open CocartesianMonoidal π’ž.U π’ž.cocartesian using (βŠ₯+--id; -+βŠ₯-id; βŠ₯+Aβ‰…A; A+βŠ₯β‰…A; +-monoidal) +open CocartesianMonoidal π’ž.cocartesian using (βŠ₯+--id; -+βŠ₯-id; βŠ₯+Aβ‰…A; A+βŠ₯β‰…A; +-monoidal) open CocartesianSymmetricMonoidal π’ž.U π’ž.cocartesian using (+-symmetric) open Monoidal +-monoidal using () renaming (triangle to tri; pentagon to pent) @@ -36,8 +36,7 @@ open import Categories.Category.Monoidal.Utilities +-monoidal using (associator- module _ where - open CartesianCategory FinitelyCocompletes-CC using (products) - open BinaryProducts products using (_Γ—_) + open CartesianCategory FinitelyCocompletes-CC using (_Γ—_) π’žΓ—π’ž : FinitelyCocompleteCategory o β„“ e π’žΓ—π’ž = π’ž Γ— π’ž diff --git a/Category/Monoidal/Instance/DecoratedCospans/Products.agda b/Category/Monoidal/Instance/DecoratedCospans/Products.agda index 647f887..4fd323e 100644 --- a/Category/Monoidal/Instance/DecoratedCospans/Products.agda +++ b/Category/Monoidal/Instance/DecoratedCospans/Products.agda @@ -21,7 +21,6 @@ import Categories.Morphism.Reasoning as β‡’-Reasoning open import Categories.Category using (_[_,_]; _[_β‰ˆ_]; _[_∘_]; Category) open import Categories.Category.Core 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.Functor using (Functor; _∘F_) renaming (id to idF) @@ -44,8 +43,7 @@ module π’Ÿ = SymmetricMonoidalCategory π’Ÿ module _ where - open CartesianCategory FinitelyCocompletes-CC using (products) - open BinaryProducts products using (_Γ—_) + open CartesianCategory FinitelyCocompletes-CC using (_Γ—_) π’žΓ—π’ž : FinitelyCocompleteCategory o β„“ e π’žΓ—π’ž = π’ž Γ— π’ž @@ -57,8 +55,7 @@ module _ where module _ where - open Cartesian SymMonCat-Cartesianβ€² using (products) - open BinaryProducts products using (_Γ—_; _⁂_) + open Cartesian SymMonCat-Cartesianβ€² using (_Γ—_) π’ŸΓ—π’Ÿ : SymmetricMonoidalCategory oβ€² β„“β€² eβ€² π’ŸΓ—π’Ÿ = π’Ÿ Γ— π’Ÿ @@ -70,8 +67,7 @@ module _ where module _ where - open Cartesian SymMonCat-Cartesian using (products) - open BinaryProducts products using (_Γ—_; _⁂_) + open Cartesian SymMonCat-Cartesian using (_Γ—_) smcπ’žΓ—π’ž : SymmetricMonoidalCategory o β„“ e smcπ’žΓ—π’ž = smc π’ž Γ— smc π’ž diff --git a/Category/Monoidal/Instance/Nat.agda b/Category/Monoidal/Instance/Nat.agda index 24b30a6..23ee39d 100644 --- a/Category/Monoidal/Instance/Nat.agda +++ b/Category/Monoidal/Instance/Nat.agda @@ -6,7 +6,9 @@ open import Level using (0β„“) open import Categories.Category.Monoidal.Bundle using (MonoidalCategory; SymmetricMonoidalCategory) open import Categories.Category.Instance.Nat using (Nat; Nat-Cartesian; Nat-Cocartesian; Natop) open import Categories.Category.Cartesian using (Cartesian) -open import Categories.Category.Cocartesian using (Cocartesian; module CocartesianMonoidal; module CocartesianSymmetricMonoidal) +open import Categories.Category.Cocartesian using (Cocartesian) +open import Categories.Category.Cocartesian.Monoidal using (module CocartesianMonoidal) +open import Categories.Category.Cocartesian.SymmetricMonoidal using (module CocartesianSymmetricMonoidal) open import Categories.Category.Cartesian.Monoidal using (module CartesianMonoidal) open import Categories.Category.Duality using (coCartesianβ‡’Cocartesian; Cocartesianβ‡’coCartesian) @@ -26,7 +28,7 @@ module Monoidal where Nat,+,0 : MonoidalCategory 0β„“ 0β„“ 0β„“ Nat,+,0 .U = Nat - Nat,+,0 .monoidal = +-monoidal Nat Nat-Cocartesian + Nat,+,0 .monoidal = +-monoidal Nat-Cocartesian Nat,Γ—,1 : MonoidalCategory 0β„“ 0β„“ 0β„“ Nat,Γ—,1 .U = Nat @@ -38,7 +40,7 @@ module Monoidal where Natop,Γ—,1 : MonoidalCategory 0β„“ 0β„“ 0β„“ Natop,Γ—,1 .U = Natop - Natop,Γ—,1 .monoidal = +-monoidal Natop Natop-Cocartesian + Natop,Γ—,1 .monoidal = +-monoidal Natop-Cocartesian module Symmetric where @@ -50,7 +52,7 @@ module Symmetric where Nat,+,0 : SymmetricMonoidalCategory 0β„“ 0β„“ 0β„“ Nat,+,0 .U = Nat - Nat,+,0 .monoidal = +-monoidal Nat Nat-Cocartesian + Nat,+,0 .monoidal = +-monoidal Nat-Cocartesian Nat,+,0 .symmetric = +-symmetric Nat Nat-Cocartesian Nat,Γ—,1 : SymmetricMonoidalCategory 0β„“ 0β„“ 0β„“ @@ -65,7 +67,7 @@ module Symmetric where Natop,Γ—,1 : SymmetricMonoidalCategory 0β„“ 0β„“ 0β„“ Natop,Γ—,1 .U = Natop - Natop,Γ—,1 .monoidal = +-monoidal Natop Natop-Cocartesian + Natop,Γ—,1 .monoidal = +-monoidal Natop-Cocartesian Natop,Γ—,1 .symmetric = +-symmetric Natop Natop-Cocartesian open Symmetric public -- cgit v1.2.3