From 1a84efec2ba0769035144782e1e96a10e0d5a7b2 Mon Sep 17 00:00:00 2001 From: Jacques Comeaux Date: Sun, 4 Jan 2026 10:59:04 -0600 Subject: Update to latest agda-categories --- Functor/Instance/Underlying/SymmetricMonoidal/FinitelyCocomplete.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'Functor/Instance/Underlying/SymmetricMonoidal') 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) -- cgit v1.2.3