1 files changed, 15 insertions, 0 deletions
diff --git a/Category/Cocomplete/Finitely/SymmetricMonoidal.agda b/Category/Cocomplete/Finitely/SymmetricMonoidal.agda
new file mode 100644
index 0000000..26813eb
--- /dev/null
+++ b/Category/Cocomplete/Finitely/SymmetricMonoidal.agda
@@ -0,0 +1,15 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Categories.Category.Core using (Category)
+
+module Category.Cocomplete.Finitely.SymmetricMonoidal {o ℓ e} {𝒞 : Category o ℓ e} where
+
+open import Categories.Category.Cocomplete.Finitely using (FinitelyCocomplete)
+open import Categories.Category.Cocartesian 𝒞 using (module CocartesianMonoidal; module CocartesianSymmetricMonoidal)
+
+
+module FinitelyCocompleteSymmetricMonoidal (finCo : FinitelyCocomplete 𝒞) where
+
+  open FinitelyCocomplete finCo using (cocartesian)
+  open CocartesianMonoidal cocartesian using (+-monoidal) public
+  open CocartesianSymmetricMonoidal cocartesian using (+-symmetric) public