Add decorated cospans

3 files changed, 42 insertions, 16 deletions

diff --git a/Category/Cocomplete/Bundle.agda b/Category/Cocomplete/Bundle.agda
deleted file mode 100644
index 3ab3cac..0000000
--- a/Category/Cocomplete/Bundle.agda
+++ /dev/null
@@ -1,16 +0,0 @@
-{-# OPTIONS --without-K --safe #-}
-module Category.Cocomplete.Bundle where
-
-open import Level
-
-open import Categories.Category.Cocomplete.Finitely using (FinitelyCocomplete)
-open import Categories.Category.Core using (Category)
-
-
-record FinitelyCocompleteCategory o ℓ e : Set (suc (o ⊔ ℓ ⊔ e)) where
-  field
-    U     : Category o ℓ e
-    finCo : FinitelyCocomplete U
-
-  open Category U public
-  open FinitelyCocomplete finCo public
diff --git a/Category/Cocomplete/Finitely/Bundle.agda b/Category/Cocomplete/Finitely/Bundle.agda
new file mode 100644
index 0000000..af40895
--- /dev/null
+++ b/Category/Cocomplete/Finitely/Bundle.agda
@@ -0,0 +1,27 @@
+{-# OPTIONS --without-K --safe #-}
+module Category.Cocomplete.Finitely.Bundle where
+
+open import Level
+open import Categories.Category.Core using (Category)
+open import Categories.Category.Cocomplete.Finitely using (FinitelyCocomplete)
+open import Category.Cocomplete.Finitely.SymmetricMonoidal using (module FinitelyCocompleteSymmetricMonoidal)
+open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory)
+
+
+record FinitelyCocompleteCategory o ℓ e : Set (suc (o ⊔ ℓ ⊔ e)) where
+
+  field
+    U     : Category o ℓ e
+    finCo : FinitelyCocomplete U
+
+  open Category U public
+  open FinitelyCocomplete finCo public
+
+  open FinitelyCocompleteSymmetricMonoidal finCo using (+-monoidal; +-symmetric)
+
+  symmetricMonoidalCategory : SymmetricMonoidalCategory o ℓ e
+  symmetricMonoidalCategory = record
+      { U = U
+      ; monoidal = +-monoidal
+      ; symmetric = +-symmetric
+      }
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