aboutsummaryrefslogtreecommitdiff
path: root/Functor/Instance/CMonoidalize.agda
diff options
context:
space:
mode:
authorJacques Comeaux <jacquesrcomeaux@protonmail.com>2026-07-10 17:21:14 -0700
committerJacques Comeaux <jacquesrcomeaux@protonmail.com>2026-07-10 17:21:14 -0700
commita408cbee9abbe2dbeee09bd36afc678efe7b6557 (patch)
tree22d6f05d6ce81357629fa2864305b81d68eed52e /Functor/Instance/CMonoidalize.agda
parent7875edd03cce586a8c9f0b95dedffb390bfdbd61 (diff)
Use latest agda-categories
Diffstat (limited to 'Functor/Instance/CMonoidalize.agda')
-rw-r--r--Functor/Instance/CMonoidalize.agda2
1 files changed, 1 insertions, 1 deletions
diff --git a/Functor/Instance/CMonoidalize.agda b/Functor/Instance/CMonoidalize.agda
index ad9b266..eef2bc8 100644
--- a/Functor/Instance/CMonoidalize.agda
+++ b/Functor/Instance/CMonoidalize.agda
@@ -12,7 +12,7 @@ module Functor.Instance.CMonoidalize
(D : SymmetricMonoidalCategory o′ ℓ′ e′)
where
-open import Categories.Category.Cocartesian using (module CocartesianSymmetricMonoidal)
+open import Categories.Category.Cocartesian.SymmetricMonoidal using (module CocartesianSymmetricMonoidal)
open import Categories.Functor using (Functor)
open import Category.Construction.CMonoids using (CMonoids)
open import Categories.Category.Construction.Functors using (Functors)