From 1a84efec2ba0769035144782e1e96a10e0d5a7b2 Mon Sep 17 00:00:00 2001 From: Jacques Comeaux Date: Sun, 4 Jan 2026 10:59:04 -0600 Subject: Update to latest agda-categories --- Category/Instance/Properties/SymMonCat.agda | 1 - Category/Instance/SymMonCat.agda | 2 +- 2 files changed, 1 insertion(+), 2 deletions(-) (limited to 'Category/Instance') diff --git a/Category/Instance/Properties/SymMonCat.agda b/Category/Instance/Properties/SymMonCat.agda index fa15295..3b49b26 100644 --- a/Category/Instance/Properties/SymMonCat.agda +++ b/Category/Instance/Properties/SymMonCat.agda @@ -18,7 +18,6 @@ open import Categories.Category.Instance.One using (One) open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory) open import Categories.Category.Cartesian SymMonCat using (Cartesian) open import Categories.Category.Cartesian.Bundle using (CartesianCategory) -open import Categories.Functor.Monoidal.Properties using (idF-SymmetricMonoidal; ∘-SymmetricMonoidal) open import Categories.Category.BinaryProducts SymMonCat using (BinaryProducts) open import Categories.Functor.Monoidal.Construction.Product using () diff --git a/Category/Instance/SymMonCat.agda b/Category/Instance/SymMonCat.agda index e4b136c..814abeb 100644 --- a/Category/Instance/SymMonCat.agda +++ b/Category/Instance/SymMonCat.agda @@ -16,7 +16,7 @@ open import Relation.Binary.Core using (Rel) open import Categories.Category using (Category; _[_,_]; _[_∘_]) open import Categories.Category.Helper using (categoryHelper) open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory) -open import Categories.Functor.Monoidal.Properties using (idF-SymmetricMonoidal; ∘-SymmetricMonoidal) +open import Categories.Functor.Monoidal.Symmetric.Properties using (idF-SymmetricMonoidal; ∘-SymmetricMonoidal) open SMF.Lax using (SymmetricMonoidalFunctor) open SMNI.Lax using (SymmetricMonoidalNaturalIsomorphism; id; isEquivalence) -- cgit v1.2.3