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/BinaryBiproducts.agda | 16 ++++++++++------
 Category/Semiadditive.agda     | 19 +++++++++++++++++++
 2 files changed, 29 insertions(+), 6 deletions(-)

(limited to 'Category')

diff --git a/Category/BinaryBiproducts.agda b/Category/BinaryBiproducts.agda
index c975d18..81a23cf 100644
--- a/Category/BinaryBiproducts.agda
+++ b/Category/BinaryBiproducts.agda
@@ -31,13 +31,11 @@ record BinaryBiproducts : Set (levelOfTerm 𝒞) where
   _⊕_ : Obj → Obj → Obj
   A ⊕ B = Biproduct.A⊕B (biproduct {A} {B})
 
-  private
-
-    binaryProducts : BinaryProducts
-    binaryProducts = record { product = Biproduct⇒Product biproduct }
+  binaryProducts : BinaryProducts
+  binaryProducts = record { product = Biproduct⇒Product biproduct }
 
-    binaryCoproducts : BinaryCoproducts
-    binaryCoproducts = record { coproduct = Biproduct⇒Coproduct biproduct }
+  binaryCoproducts : BinaryCoproducts
+  binaryCoproducts = record { coproduct = Biproduct⇒Coproduct biproduct }
 
   open BinaryProducts binaryProducts public
     hiding (_×_)
@@ -276,6 +274,12 @@ record BinaryBiproducts : Set (levelOfTerm 𝒞) where
       ∇ ∘ f +₁ f  ≈⟨ refl⟩∘⟨ ×₁-+₁ f f ⟨
       ∇ ∘ f ×₁ f  ∎
 
+  ∇∘×₁ : {A B C : Obj} {f : A ⇒ C} {g : B ⇒ C} → ∇ ∘ f ×₁ g ≈ [ f , g ]
+  ∇∘×₁ {f = f} {g} = begin
+      ∇ ∘ f ×₁ g  ≈⟨ refl⟩∘⟨ ×₁-+₁ f g ⟩
+      ∇ ∘ f +₁ g  ≈⟨ ∇∘+₁ ⟩
+      [ f , g ]   ∎
+
   ×₁∘first : {A B C D E : Obj} {f : B ⇒ C} {g : D ⇒ E} {h : A ⇒ B} → (f ×₁ g) ∘ first h ≈ (f ∘ h) ×₁ g
   ×₁∘first = ×₁∘×₁ ○ ×₁-cong₂ Equiv.refl identityʳ
 
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