Category of decorated cospans is symmetric monoidal

1 files changed, 16 insertions, 0 deletions

diff --git a/Category/Cartesian/Instance/SymMonCat.agda b/Category/Cartesian/Instance/SymMonCat.agda
new file mode 100644
index 0000000..7d91d52
--- /dev/null
+++ b/Category/Cartesian/Instance/SymMonCat.agda
@@ -0,0 +1,16 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Level using (Level; suc; _⊔_)
+
+module Category.Cartesian.Instance.SymMonCat {o ℓ e : Level} where
+
+open import Category.Instance.SymMonCat {o} {ℓ} {e} using (SymMonCat)
+open import Category.Instance.Properties.SymMonCat {o} {ℓ} {e} using (SymMonCat-Cartesian)
+open import Categories.Category.Cartesian.Bundle using (CartesianCategory)
+
+SymMonCat-CC : CartesianCategory (suc (o ⊔ ℓ ⊔ e)) (o ⊔ ℓ ⊔ e) (o ⊔ ℓ ⊔ e)
+SymMonCat-CC = record
+    { U = SymMonCat
+    ; cartesian = SymMonCat-Cartesian
+    }
+