From 9a65579633967a0c02b912e6baa3e575a02b868f Mon Sep 17 00:00:00 2001
From: Jacques Comeaux <jacquesrcomeaux@protonmail.com>
Date: Sat, 15 Aug 2026 12:34:15 -0500
Subject: Add monoidal structure to system functor

---
 Category/Dagger/Semiadditive.agda | 44 +++++++++++++++++++++++++++++++++++++--
 1 file changed, 42 insertions(+), 2 deletions(-)

(limited to 'Category')

diff --git a/Category/Dagger/Semiadditive.agda b/Category/Dagger/Semiadditive.agda
index adcf6ed..41be19e 100644
--- a/Category/Dagger/Semiadditive.agda
+++ b/Category/Dagger/Semiadditive.agda
@@ -11,8 +11,11 @@ import Category.Semiadditive.Monoidal as SemiadditiveMonoidal
 
 open import Categories.Category.Dagger using (HasDagger)
 open import Categories.Category.Monoidal using (Monoidal)
+open import Categories.Category.Monoidal.Braided using (Braided)
+open import Categories.Category.Monoidal.Symmetric using (Symmetric)
 open import Categories.Category.Monoidal.Bundle using (MonoidalCategory; SymmetricMonoidalCategory)
-open import Categories.Functor.Bifunctor using (Bifunctor)
+open import Categories.NaturalTransformation.NaturalIsomorphism using (_≃_; niHelper)
+open import Categories.Functor.Bifunctor using (Bifunctor; flip-bifunctor)
 open import Categories.Morphism using (Iso)
 open import Categories.Morphism.Properties 𝒞 using (Iso-resp-≈; Iso-swap)
 open import Category.Dagger.2-Poset using (Dagger-2-Poset; Map; Maps; unitary-isMap)
@@ -272,9 +275,10 @@ record IdempotentSemiadditiveDagger : Set (suc (o ⊔ ℓ ⊔ e)) where
   maps = Maps dagger-2-poset
 
   open Dagger-2-Poset dagger-2-poset using (category)
-  open SemiadditiveMonoidal semiadditive using (monoidal)
+  open SemiadditiveMonoidal semiadditive using (monoidal; symmetric)
 
   module M = Monoidal monoidal
+  module SM = Symmetric symmetric
 
   ×₁-functional
       : {A B C D : Obj}
@@ -392,8 +396,44 @@ record IdempotentSemiadditiveDagger : Set (suc (o ⊔ ℓ ⊔ e)) where
       ; M
       }
 
+  swap-unitary : {X Y : Obj} → Iso category (swap {X} {Y}) (swap †)
+  swap-unitary {X} {Y} = record { Iso (Iso-resp-≈ (SM.braiding.iso (X , Y)) refl (sym swap†)) }
+
+  swap-map : {X Y : Obj} → Map dagger-2-poset (X ⊕ Y) (Y ⊕ X)
+  swap-map = record
+      { map = swap
+      ; isMap = unitary-isMap dagger-2-poset swap-unitary
+      }
+
+  σ : ⊗ ≃ flip-bifunctor ⊗
+  σ = niHelper record
+      { η = λ _ → swap-map
+      ; η⁻¹ = λ _ → swap-map
+      ; commute = λ _ → swap∘×₁
+      ; iso = λ X → record { SM.braiding.iso X }
+      }
+
+  maps-braided : Braided maps-monoidal
+  maps-braided = record
+      { braiding = σ
+      ; SM
+      }
+
+  maps-symmetric : Symmetric maps-monoidal
+  maps-symmetric = record
+      { braided = maps-braided
+      ; SM
+      }
+
   maps-MC : MonoidalCategory o (ℓ ⊔ e) e
   maps-MC = record
       { U = maps
       ; monoidal = maps-monoidal
       }
+
+  maps-SMC : SymmetricMonoidalCategory o (ℓ ⊔ e) e
+  maps-SMC = record
+      { U = maps
+      ; monoidal = maps-monoidal
+      ; symmetric = maps-symmetric
+      }
-- 
cgit v1.2.3