aboutsummaryrefslogtreecommitdiff
path: root/Category/Instance/Properties
diff options
context:
space:
mode:
authorJacques Comeaux <jacquesrcomeaux@protonmail.com>2026-01-04 10:59:04 -0600
committerJacques Comeaux <jacquesrcomeaux@protonmail.com>2026-01-04 10:59:04 -0600
commit1a84efec2ba0769035144782e1e96a10e0d5a7b2 (patch)
tree2be1a8bc1f809794b097320861c59b0b45cc689a /Category/Instance/Properties
parentf84a8d1bf9525aa9a005c1a31045b7685c6ac059 (diff)
Update to latest agda-categories
Diffstat (limited to 'Category/Instance/Properties')
-rw-r--r--Category/Instance/Properties/SymMonCat.agda1
1 files changed, 0 insertions, 1 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 ()