diff options
| author | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2026-01-04 10:59:04 -0600 |
|---|---|---|
| committer | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2026-01-04 10:59:04 -0600 |
| commit | 1a84efec2ba0769035144782e1e96a10e0d5a7b2 (patch) | |
| tree | 2be1a8bc1f809794b097320861c59b0b45cc689a /Category/Instance | |
| parent | f84a8d1bf9525aa9a005c1a31045b7685c6ac059 (diff) | |
Update to latest agda-categories
Diffstat (limited to 'Category/Instance')
| -rw-r--r-- | Category/Instance/Properties/SymMonCat.agda | 1 | ||||
| -rw-r--r-- | Category/Instance/SymMonCat.agda | 2 |
2 files changed, 1 insertions, 2 deletions
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) |