From f7afdb1823fe8d785849f817d022efa100007560 Mon Sep 17 00:00:00 2001
From: Jacques Comeaux <jacquesrcomeaux@protonmail.com>
Date: Wed, 23 Apr 2025 10:09:32 -0500
Subject: Category of decorated cospans is symmetric monoidal

---
 Category/Cartesian/Instance/SymMonCat.agda | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)
 create mode 100644 Category/Cartesian/Instance/SymMonCat.agda

(limited to 'Category/Cartesian/Instance/SymMonCat.agda')

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
+    }
+
-- 
cgit v1.2.3