From 776ec567fd788ddef1f7617b7a3bfeb9cf46c28d Mon Sep 17 00:00:00 2001
From: Jacques Comeaux <jacquesrcomeaux@protonmail.com>
Date: Thu, 30 Jul 2026 15:44:41 -0700
Subject: Show category of directed wiring diagrams is monoidal

---
 Category/Semiadditive.agda | 19 +++++++++++++++++++
 1 file changed, 19 insertions(+)

(limited to 'Category/Semiadditive.agda')

diff --git a/Category/Semiadditive.agda b/Category/Semiadditive.agda
index 9bbc9c7..05ce264 100644
--- a/Category/Semiadditive.agda
+++ b/Category/Semiadditive.agda
@@ -6,9 +6,13 @@ open import Categories.Category using (Category)
 module Category.Semiadditive {o ℓ e : Level} (𝒞 : Category o ℓ e) where
 
 import Categories.Morphism.Reasoning 𝒞 as ⇒-Reasoning
+import Categories.Category.Cartesian.SymmetricMonoidal 𝒞 as CartesianSymmetricMonoidal
 
 open import Algebra using (IsCommutativeMonoid; CommutativeMonoid)
 open import Categories.Category.CMonoidEnriched using (CM-Category)
+open import Categories.Category.Cartesian 𝒞 using (Cartesian)
+open import Categories.Category.Cartesian.Monoidal using (module CartesianMonoidal)
+open import Categories.Category.Cocartesian 𝒞 using (Cocartesian)
 open import Categories.Object.Zero 𝒞 using (Zero)
 open import Category.BinaryBiproducts 𝒞 using (BinaryBiproducts)
 open import Data.Product using (_,_)
@@ -160,3 +164,18 @@ record Semiadditive : Set (levelOfTerm 𝒞) where
       ; +-resp-∘ = +-resp-∘
       ; 0-resp-∘ = 0-resp-∘
       }
+
+  cartesian : Cartesian
+  cartesian = record
+      { terminal = terminal
+      ; products = binaryProducts
+      }
+
+  cocartesian : Cocartesian
+  cocartesian = record
+      { initial = initial
+      ; coproducts = binaryCoproducts
+      }
+
+  open CartesianMonoidal cartesian using (monoidal) public
+  open CartesianSymmetricMonoidal cartesian using (symmetric) public
-- 
cgit v1.2.3