diff options
Diffstat (limited to 'Functor/Instance/Underlying/SymmetricMonoidal/FinitelyCocomplete.agda')
| -rw-r--r-- | Functor/Instance/Underlying/SymmetricMonoidal/FinitelyCocomplete.agda | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Functor/Instance/Underlying/SymmetricMonoidal/FinitelyCocomplete.agda b/Functor/Instance/Underlying/SymmetricMonoidal/FinitelyCocomplete.agda index 80b7b2f..77064ba 100644 --- a/Functor/Instance/Underlying/SymmetricMonoidal/FinitelyCocomplete.agda +++ b/Functor/Instance/Underlying/SymmetricMonoidal/FinitelyCocomplete.agda @@ -12,7 +12,7 @@ open import Categories.Functor using (Functor; _∘F_) open import Categories.Functor.Properties using ([_]-resp-square; [_]-resp-∘) open import Categories.Functor.Monoidal using (IsMonoidalFunctor) open import Categories.Functor.Monoidal.Braided using (module Lax) -open import Categories.Functor.Monoidal.Properties using (idF-SymmetricMonoidal; ∘-SymmetricMonoidal) +open import Categories.Functor.Monoidal.Symmetric.Properties using (idF-SymmetricMonoidal; ∘-SymmetricMonoidal) open import Categories.Functor.Monoidal.Symmetric using (module Lax) open import Categories.Category using (Category; _[_,_]; _[_≈_]; _[_∘_]) open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory; BraidedMonoidalCategory; MonoidalCategory) |