aboutsummaryrefslogtreecommitdiff
path: root/Functor/Monoidal/Construction/CMonoidValued.agda
diff options
context:
space:
mode:
Diffstat (limited to 'Functor/Monoidal/Construction/CMonoidValued.agda')
-rw-r--r--Functor/Monoidal/Construction/CMonoidValued.agda2
1 files changed, 1 insertions, 1 deletions
diff --git a/Functor/Monoidal/Construction/CMonoidValued.agda b/Functor/Monoidal/Construction/CMonoidValued.agda
index 2ac8be2..eb5c965 100644
--- a/Functor/Monoidal/Construction/CMonoidValued.agda
+++ b/Functor/Monoidal/Construction/CMonoidValued.agda
@@ -24,7 +24,7 @@ import Categories.Morphism.Reasoning as ⇒-Reasoning
import Object.Monoid.Commutative as CommutativeMonoidObject
import Functor.Monoidal.Construction.MonoidValued as MonoidValued
-open import Categories.Category.Cocartesian using (module CocartesianSymmetricMonoidal)
+open import Categories.Category.Cocartesian.SymmetricMonoidal using (module CocartesianSymmetricMonoidal)
open import Categories.Category.Cocartesian.Bundle using (CocartesianCategory)
open import Categories.Category.Construction.Monoids using (Monoids)
open import Categories.Category.Monoidal.Symmetric.Properties using (module Shorthands)