Add monoidal structure to system functor

2 files changed, 485 insertions, 7 deletions

diff --git a/Functor/Instance/WiringDiagram/System.agda b/Functor/Instance/WiringDiagram/System.agda
index 80a4fe5..891787b 100644
--- a/Functor/Instance/WiringDiagram/System.agda
+++ b/Functor/Instance/WiringDiagram/System.agda
@@ -11,7 +11,7 @@ open import Category.Instance.CMonoids using (CMonoids; CMonoidHomomorphism)
 open import Level using (Level; suc)
 
 module Functor.Instance.WiringDiagram.System
-    {o ℓ e o′ ℓ′ e′ : Level}
+    {o ℓ e : Level}
     {c : Level}
     {𝒞 : Category o ℓ e}
     {S : IdempotentSemiadditiveDagger 𝒞}
@@ -24,6 +24,7 @@ import Data.System.Monoidal as Sys-⊗
 import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
 
 open import Algebra using (CommutativeMonoid)
+open import Algebra.Construct.DirectProduct using () renaming (commutativeMonoid to _×ₘ_)
 open import Categories.Category.Cartesian using (Cartesian)
 open import Categories.Category.CartesianClosed using (CartesianClosed)
 open import Categories.Category.Instance.Properties.Setoids.CCC using (Setoids-CCC)
@@ -32,6 +33,8 @@ open import Categories.Category.Product using (_⁂_)
 open import Categories.Functor.Cartesian.Properties using (isMonoidalFunctor)
 open import Categories.Functor.Monoidal using (MonoidalFunctor)
 open import Categories.Functor.Monoidal.Symmetric using (module Lax)
+open import Categories.Functor.Properties using ([_]-resp-≅)
+open import Categories.Morphism using (module ≅)
 open import Categories.Morphism.Reasoning.Iso (CMonoids c c) using (switch-fromtoˡ)
 open import Categories.NaturalTransformation.NaturalIsomorphism using (_≃_; niHelper)
 open import Categories.Object.Product (CMonoids c c) using (Product; IsProduct)
@@ -94,6 +97,61 @@ _⟦⊕⟧_ {A} {B} a b = ⟦ F.×-iso.to A B ⟧ (a , b)
     ⊗-F = isMonoidalFunctor {C = 𝒞-CC} {CMonoids-CC {c} {c}} F
     module ⊗-F = MonoidalFunctor ⊗-F
 
+⟦⊕⟧-assocˡ
+    : {A B C : Obj}
+      (a : Carrier (F.₀ A))
+      (b : Carrier (F.₀ B))
+      (c : Carrier (F.₀ C))
+    → (let open CommutativeMonoid (F.₀ (A ⊕ (B ⊕ C))) using (_≈_))
+    → ⟦ F.₁ S.assocˡ ⟧ ((a ⟦⊕⟧ b) ⟦⊕⟧ c) ≈ a ⟦⊕⟧ (b ⟦⊕⟧ c)
+⟦⊕⟧-assocˡ {A} {B} {C} a b c- = begin
+    ⟦ F.₁ S.assocˡ ⟧ ((a ⟦⊕⟧ b) ⟦⊕⟧ c-) ≈⟨ ⊗-F.associativity ((a , b) , c-) ⟩
+    a ⟦⊕⟧ (b ⟦⊕⟧ c-)                    ∎
+  where
+    open ≈-Reasoning (setoid (F.₀ (A ⊕ (B ⊕ C))))
+    module 𝒞-CC = CartesianCategory 𝒞-CC
+    ⊗-F : MonoidalFunctor 𝒞-CC.monoidalCategory (CMonoids-CC.monoidalCategory {c} {c})
+    ⊗-F = isMonoidalFunctor {C = 𝒞-CC} {CMonoids-CC {c} {c}} F
+    module ⊗-F = MonoidalFunctor ⊗-F
+
+⟦⊕⟧-assocʳ
+    : {A B C : Obj}
+      (a : Carrier (F.₀ A))
+      (b : Carrier (F.₀ B))
+      (c : Carrier (F.₀ C))
+    → (let open CommutativeMonoid (F.₀ ((A ⊕ B) ⊕ C)) using (_≈_))
+    → ⟦ F.₁ S.assocʳ ⟧ (a ⟦⊕⟧ (b ⟦⊕⟧ c)) ≈ (a ⟦⊕⟧ b) ⟦⊕⟧ c
+⟦⊕⟧-assocʳ {A} {B} {C} a b c- = begin
+    ⟦ F.₁ S.assocʳ ⟧ (a ⟦⊕⟧ (b ⟦⊕⟧ c-)) ≈⟨ switch-fromtoˡ ([ F.F ]-resp-≅ (≅.sym 𝒞 S.⊕-assoc)) {h = h} {k = k} ⊗-F.associativity ((a , b) , c-) ⟨
+    (a ⟦⊕⟧ b) ⟦⊕⟧ c-                    ∎
+  where
+    open ≈-Reasoning (setoid (F.₀ ((A ⊕ B) ⊕ C)))
+    module 𝒞-CC = CartesianCategory 𝒞-CC
+    ⊗-F : MonoidalFunctor 𝒞-CC.monoidalCategory (CMonoids-CC.monoidalCategory {c} {c})
+    ⊗-F = isMonoidalFunctor {C = 𝒞-CC} {CMonoids-CC {c} {c}} F
+    module ⊗-F = MonoidalFunctor ⊗-F
+    h : CMonoidHomomorphism c c ((F.₀ A ×ₘ F.₀ B) ×ₘ F.₀ C) (F.₀ ((A ⊕ B) ⊕ C))
+    h = ⊗-F.⊗-homo.η (A ⊕ B , C) CMonoids-CC.∘ (⊗-F.⊗-homo.η (A , B) CMonoids-CC.×₁ CMonoids-CC.id)
+    k : CMonoidHomomorphism c c ((F.₀ A ×ₘ F.₀ B) ×ₘ F.₀ C) (F.₀ (A ⊕ (B ⊕ C)))
+    k = ⊗-F.⊗-homo.η (A , B ⊕ C) CMonoids-CC.∘ (CMonoids-CC.id CMonoids-CC.×₁ ⊗-F.⊗-homo.η (B , C)) CMonoids-CC.∘ CMonoids-CC.assocˡ
+
+⟨⟩-⟦⊕⟧
+    : {A B C : Obj}
+      {f : A ⇒ B}
+      {g : A ⇒ C}
+      (a : Carrier (F.₀ A))
+    → (let open CommutativeMonoid (F.₀ (B ⊕ C)) using (_≈_))
+    → ⟦ F.₁ S.⟨ f , g ⟩ ⟧ a ≈ ⟦ F.₁ f ⟧ a ⟦⊕⟧ ⟦ F.₁ g ⟧ a
+⟨⟩-⟦⊕⟧ {A} {B} {C} {f} {g} a = begin
+    ⟦ F.₁ S.⟨ f , g ⟩ ⟧ a       ≈⟨ switch-fromtoˡ (F.×-iso B C) {h = h} {k = k} (F.F-resp-⟨⟩ f g) a ⟩
+    ⟦ F.₁ f ⟧ a ⟦⊕⟧ ⟦ F.₁ g ⟧ a ∎
+  where
+    h : CMonoidHomomorphism c c (F.₀ A) (F.₀ (B ⊕ C))
+    h = F.₁ S.⟨ f , g ⟩
+    k : CMonoidHomomorphism c c (F.₀ A) _
+    k = CMonoids-CC.⟨ F.₁ f , F.₁ g ⟩
+    open ≈-Reasoning (setoid (F.₀ (B ⊕ C)))
+
 ⟦⊕⟧-congˡ
     : {A B : Obj}
       (let module FB = CommutativeMonoid (F.₀ B))
@@ -243,14 +301,10 @@ homomorphism {Xᵢ} {Xₒ} {Yᵢ} {Yₒ} {Zᵢ} {Zₒ} {fᵢ} {fₒ} {gᵢ} {g�
             → ⟦ F.₁ S.⟨ S.π₁ , 𝒞.id ⟩ ⟧ (X.fₒ′ s ⟦⊕⟧ i)
             ≈ X.fₒ′ s ⟦⊕⟧ (X.fₒ′ s ⟦⊕⟧ i)
         lem₂ = begin
-            ⟦ F.₁ S.⟨ S.π₁ , 𝒞.id ⟩ ⟧ (X.fₒ′ s ⟦⊕⟧ i)       ≈⟨ switch-fromtoˡ (F.×-iso Xₒ (Xₒ ⊕ Zᵢ)) {h = h} {k = k} (F.F-resp-⟨⟩ S.π₁ 𝒞.id) (X.fₒ′ s ⟦⊕⟧ i) ⟩
-            ⟦ F.₁ S.π₁ ⟧ (X.fₒ′ s ⟦⊕⟧ i) ⟦⊕⟧ ⟦ F.₁ 𝒞.id ⟧ (X.fₒ′ s ⟦⊕⟧ i) ≈⟨ ⟦⊕⟧-cong (F.F-resp-×.project₁ (X.fₒ′ s , i)) (F.identity (X.fₒ′ s ⟦⊕⟧ i)) ⟩
+            ⟦ F.₁ S.⟨ S.π₁ , 𝒞.id ⟩ ⟧ (X.fₒ′ s ⟦⊕⟧ i)       ≈⟨ ⟨⟩-⟦⊕⟧ (X.fₒ′ s ⟦⊕⟧ i) ⟩
+            ⟦ F.₁ S.π₁ ⟧ _ ⟦⊕⟧ ⟦ F.₁ 𝒞.id ⟧ (X.fₒ′ s ⟦⊕⟧ i) ≈⟨ ⟦⊕⟧-cong (F.F-resp-×.project₁ (X.fₒ′ s , i)) (F.identity (X.fₒ′ s ⟦⊕⟧ i)) ⟩
             X.fₒ′ s ⟦⊕⟧ (X.fₒ′ s ⟦⊕⟧ i)                     ∎
           where
-            h : CMonoidHomomorphism c c (F.₀ (Xₒ ⊕ Zᵢ)) (F.₀ (Xₒ ⊕ (Xₒ ⊕ Zᵢ)))
-            h = F.₁ _
-            k : CMonoidHomomorphism c c (F.₀ (Xₒ ⊕ Zᵢ)) _
-            k = CMonoids-CC.⟨ F.₁ _ , F.₁ _ ⟩
             open ≈-Reasoning (setoid (F.₀ (Xₒ ⊕ (Xₒ ⊕ Zᵢ))))
         lem₃
             : (let open CommutativeMonoid (F.₀ (Xₒ ⊕ Yᵢ)) using (_≈_))
@@ -341,3 +395,5 @@ Sys = record
     ; homomorphism = homomorphism
     ; F-resp-≈ = Sys-resp-≈
     }
+
+module Sys = Functor Sys
diff --git a/Functor/Monoidal/Instance/WiringDiagram/System.agda b/Functor/Monoidal/Instance/WiringDiagram/System.agda
new file mode 100644
index 0000000..786b221
--- /dev/null
+++ b/Functor/Monoidal/Instance/WiringDiagram/System.agda
@@ -0,0 +1,422 @@
+{-# OPTIONS --without-K --safe #-}
+{-# OPTIONS --lossy-unification #-}
+
+open import Categories.Category using (Category)
+open import Categories.Category.Cartesian.Bundle using (CartesianCategory)
+open import Categories.Category.Instance.Cats using (Cats)
+open import Categories.Functor using (Functor; _∘F_) renaming (id to IdF)
+open import Categories.Functor.Cartesian using (CartesianF)
+open import Category.Cartesian.Instance.CMonoids using (CMonoids-CC)
+open import Category.Dagger.Semiadditive using (IdempotentSemiadditiveDagger)
+open import Category.Instance.CMonoids using (CMonoids; CMonoidHomomorphism)
+open import Level using (Level; suc)
+
+module Functor.Monoidal.Instance.WiringDiagram.System
+    {o ℓ e o′ ℓ′ e′ : Level}
+    {c : Level}
+    {𝒞 : Category o ℓ e}
+    {S : IdempotentSemiadditiveDagger 𝒞}
+    (let private module S = IdempotentSemiadditiveDagger S)
+    (let 𝒞-CC = record { cartesian = S.cartesian })
+    (F : CartesianF 𝒞-CC (CMonoids-CC {c} {c}))
+  where
+
+import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
+
+open import Algebra using (CommutativeMonoid)
+open import Algebra.Construct.DirectProduct using () renaming (commutativeMonoid to _×ₘ_)
+open import Categories.Category.Cartesian using (Cartesian)
+open import Categories.Category.Cartesian.Monoidal using (module CartesianMonoidal)
+open import Categories.Category.CartesianClosed using (CartesianClosed)
+open import Categories.Category.Instance.Cats using (Cats)
+open import Categories.Category.Instance.One using (One)
+open import Categories.Category.Instance.Properties.Setoids.CCC using (Setoids-CCC)
+open import Categories.Category.Instance.Setoids using (Setoids)
+open import Categories.Category.Monoidal.Bundle using (MonoidalCategory)
+open import Categories.Category.Monoidal.Instance.Cats using (module Product)
+open import Categories.Category.Product using (_※_; _⁂_; πˡ; πʳ)
+open import Categories.Functor.Bifunctor using (Bifunctor)
+open import Categories.Functor.Monoidal using (IsMonoidalFunctor; MonoidalFunctor)
+open import Categories.Morphism using (module ≅)
+open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper)
+open import Categories.NaturalTransformation.NaturalIsomorphism using (_≃_; niHelper)
+open import Categories.NaturalTransformation.NaturalIsomorphism.Properties using (pointwise-iso)
+open import Data.Product using (_,_)
+open import Data.Product using (proj₁; proj₂)
+open import Data.Product.Function.NonDependent.Setoid using (_×-function_; proj₁ₛ; proj₂ₛ; <_,_>ₛ)
+open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_)
+open import Data.Setoid using (∣_∣)
+open import Data.System using (discrete; ≤-refl; System; _≤_; mk-≅)
+open import Data.Unit.Polymorphic using (tt)
+open import Data.WiringDiagram.Core S.semiadditiveDagger using (Box; _□_; WiringDiagram)
+open import Data.WiringDiagram.Monoidal S.semiadditiveDagger using (DWD-MC)
+open import Data.WiringDiagram.Monoidal.Core S.semiadditiveDagger using (𝟘-□; _⊞_; _⊞₁_; module Directed)
+open import Function using (_⟨$⟩_; Func)
+open import Function.Construct.Identity using () renaming (function to Id)
+open import Function.Construct.Setoid using (_∙_)
+open import Functor.Instance.WiringDiagram.System {S = S} F using (wire; Sys; _⟦⊕⟧_; ⟦⊕⟧-cong; ⟦⊕⟧-congˡ; ⟦⊕⟧-commute; ⟦⊕⟧-assocˡ; ⟦⊕⟧-assocʳ; ⟨⟩-⟦⊕⟧; Wire)
+open import Relation.Binary using (Setoid)
+
+module F = CartesianF F
+module Setoids-CC = CartesianClosed (Setoids-CCC c)
+
+open CMonoidHomomorphism using (⟦_⟧; func; ⟦⟧-cong)
+open Cartesian Setoids-CC.cartesian using (×-assoc; assocˡ; assocʳ)
+open Category 𝒞 hiding (_≈_)
+open CommutativeMonoid using (setoid; Carrier)
+open Directed using (-⊞-)
+open S using (_⊕_; _×₁_; σ₂₃)
+
+Cats-MC : MonoidalCategory (suc (suc c)) (suc c) (suc c)
+Cats-MC = record
+    { U = Cats (suc c) c c
+    ; monoidal = Product.Cats-Monoidal
+    }
+
+module Cats-MC = MonoidalCategory Cats-MC
+module Cats-C = Cartesian Product.Cats-is
+
+ε : Functor (One {suc c} {c} {c}) (Sys.₀ 𝟘-□)
+ε = record
+    { F₀ = λ _ → discrete (setoid (F.₀ S.𝟘)) (F.₀ S.𝟘)
+    ; F₁ = λ _ → ≤-refl
+    ; identity = tt
+    ; homomorphism = tt
+    ; F-resp-≈ = λ _ → tt
+    }
+
+×-System
+    : {A B C D : Obj}
+    → System (setoid (F.₀ A)) (F.₀ B)
+    → System (setoid (F.₀ C)) (F.₀ D)
+    → System (setoid (F.₀ (A ⊕ C))) (F.₀ (B ⊕ D))
+×-System {A} {B} {C} {D} X Y = record
+    { S = X.S ×ₛ Y.S
+    ; fₛ = λg (< eval ∙ (X.fₛ ∙ proj₁ₛ) ×-function proj₁ₛ , eval ∙ (Y.fₛ ∙ proj₂ₛ) ×-function proj₂ₛ >ₛ) ∙ func (F.×-iso.from A C)
+    ; fₒ = func (F.×-iso.to B D) ∙ X.fₒ ×-function Y.fₒ
+    }
+  where
+    module X = System X
+    module Y = System Y
+    open CartesianClosed (Setoids-CCC c) using (λg; eval; cartesian)
+    open Cartesian cartesian using (π₁; π₂; ⟨_,_⟩)
+
+≤-×-System
+    : {A B C D : Obj}
+      {X X′ : System (setoid (F.₀ A)) (F.₀ B)}
+      {Y Y′ : System (setoid (F.₀ C)) (F.₀ D)}
+    → X ≤ X′
+    → Y ≤ Y′
+    → ×-System X Y ≤ ×-System X′ Y′
+≤-×-System {A} {B} {C} {D} {X} {X′} {Y} {Y′} ≤X ≤Y = record
+    { ⇒S = ≤X.⇒S ×-function ≤Y.⇒S
+    ; ≗-fₛ = λ i (s₁ , s₂) → ≤X.≗-fₛ (⟦ F.₁ S.π₁ ⟧ i) s₁ , ≤Y.≗-fₛ (⟦ F.₁ S.π₂ ⟧ i) s₂
+    ; ≗-fₒ = λ (s₁ , s₂) → ⟦⊕⟧-cong (≤X.≗-fₒ s₁) (≤Y.≗-fₒ s₂)
+    }
+  where
+    module ≤X = _≤_ ≤X
+    module ≤Y = _≤_ ≤Y
+    module X = System X
+    module Y = System Y
+    module X′ = System X′
+    module Y′ = System Y′
+    module X⊗Y = System (×-System X Y)
+    module X⊗Y′ = System (×-System X′ Y′)
+    open CommutativeMonoid (F.₀ (B ⊕ D)) using (_≈_)
+
+η : (X Y : Box) → Bifunctor (Sys.₀ X) (Sys.₀ Y) (Sys.₀ (X ⊞ Y))
+η X Y = record
+    { F₀ = λ (x , y) → ×-System x y
+    ; F₁ = λ (f , g) → ≤-×-System f g
+    ; identity = λ {(A , B)} → S.refl A , S.refl B
+    ; homomorphism = λ {_ _ (Z , Z′)} → S.refl Z , S.refl Z′
+    ; F-resp-≈ = λ (≈f , ≈g) → ≈f , ≈g
+    }
+  where
+    open System using (S)
+
+module Commute
+    {A A′ B B′ C C′ D D′ : Obj}
+    (f : WiringDiagram (A □ B) (A′ □ B′))
+    (g : WiringDiagram (C □ D) (C′ □ D′))
+    (X : System (setoid (F.₀ A)) (F.₀ B))
+    (Y : System (setoid (F.₀ C)) (F.₀ D))
+  where
+    open WiringDiagram
+    fᵢ : B ⊕ A′ ⇒ A
+    fᵢ = input f
+    fₒ : B ⇒ B′
+    fₒ = output f
+    gᵢ : D ⊕ C′ ⇒ C
+    gᵢ = input g
+    gₒ : D ⇒ D′
+    gₒ = output g
+    module X = System X
+    module Y = System Y
+    module X⊗Y = System (×-System X Y)
+    module B⊗D = CommutativeMonoid (F.₀ (B′ ⊕ D′))
+    open System using (fₛ′; fₒ′)
+    module _  (s : ∣ X⊗Y.S ∣) where
+      open CartesianClosed (Setoids-CCC c) using (λg; eval)
+      open Func using (cong)
+      s₁ : ∣ X.S ∣
+      s₁ = proj₁ s
+      s₂ : ∣ Y.S ∣
+      s₂ = proj₂ s
+      ≗-fₛ
+          : (i : Carrier (F.₀ (A′ ⊕ C′)))
+          → (fₛ′ (wire fᵢ fₒ X) (⟦ F.₁ S.π₁ ⟧ i) s₁ , fₛ′ (wire gᵢ gₒ Y) (⟦ F.₁ S.π₂ ⟧ i) s₂)
+          X⊗Y.S.≈ X⊗Y.fₛ′ (⟦ F.₁ (fᵢ ×₁ gᵢ ∘ σ₂₃) ⟧ ((X.fₒ′ s₁ ⟦⊕⟧ Y.fₒ′ s₂) ⟦⊕⟧ i)) (s₁ , s₂)
+      ≗-fₛ i = let open ≈-Reasoning X⊗Y.S in begin
+          X.fₛ′ (⟦ F.₁ fᵢ ⟧ (X.fₒ′ s₁ ⟦⊕⟧ i₁)) s₁ , Y.fₛ′ (⟦ F.₁ gᵢ ⟧ (Y.fₒ′ s₂ ⟦⊕⟧ i₂)) s₂
+              ≈⟨ cong
+                    (λg (< eval ∙ (X.fₛ ∙ proj₁ₛ) ×-function proj₁ₛ , eval ∙ (Y.fₛ ∙ proj₂ₛ) ×-function proj₂ₛ >ₛ))
+                    (F.×-iso.isoʳ A C (⟦ F.₁ fᵢ ⟧ (X.fₒ′ s₁ ⟦⊕⟧ i₁) , ⟦ F.₁ gᵢ ⟧ (Y.fₒ′ s₂ ⟦⊕⟧ i₂))) ⟨
+          X⊗Y.fₛ′ (⟦ F.₁ fᵢ ⟧ (X.fₒ′ s₁ ⟦⊕⟧ i₁) ⟦⊕⟧ ⟦ F.₁ gᵢ ⟧ (Y.fₒ′ s₂ ⟦⊕⟧ i₂)) (s₁ , s₂)
+              ≈⟨ cong X⊗Y.fₛ (⟦⊕⟧-commute (X.fₒ′ s₁ ⟦⊕⟧ i₁) (Y.fₒ′ s₂ ⟦⊕⟧ i₂)) ⟨
+          X⊗Y.fₛ′ (⟦ F.₁ (fᵢ ×₁ gᵢ) ⟧ ((X.fₒ′ s₁ ⟦⊕⟧ i₁) ⟦⊕⟧ (Y.fₒ′ s₂ ⟦⊕⟧ i₂))) (s₁ , s₂)
+              ≈⟨ cong X⊗Y.fₛ (⟦⟧-cong (F.₁ (fᵢ ×₁ gᵢ))
+                  (⟦⊕⟧-cong
+                    (⟦⊕⟧-cong (F.F-resp-×.project₁ (X.fₒ′ s₁ , Y.fₒ′ s₂)) (F.F-resp-×.project₁ (i₁ , i₂)))
+                    (⟦⊕⟧-cong (F.F-resp-×.project₂ (X.fₒ′ s₁ , Y.fₒ′ s₂)) (F.F-resp-×.project₂ (i₁ , i₂))))) ⟨
+          X⊗Y.fₛ′ (⟦ F.₁ (fᵢ ×₁ gᵢ) ⟧
+              (((⟦ F.₁ S.π₁ ⟧ (X.fₒ′ s₁ ⟦⊕⟧ Y.fₒ′ s₂)) ⟦⊕⟧ (⟦ F.₁ S.π₁ ⟧ (i₁ ⟦⊕⟧ i₂))) ⟦⊕⟧
+               ((⟦ F.₁ S.π₂ ⟧ (X.fₒ′ s₁ ⟦⊕⟧ Y.fₒ′ s₂)) ⟦⊕⟧ (⟦ F.₁ S.π₂ ⟧ (i₁ ⟦⊕⟧ i₂))))) (s₁ , s₂)
+              ≈⟨ cong X⊗Y.fₛ (⟦⟧-cong (F.₁ (fᵢ ×₁ gᵢ))
+                  (⟦⊕⟧-cong
+                    (⟦⊕⟧-commute (X.fₒ′ s₁ ⟦⊕⟧ Y.fₒ′ s₂) (i₁ ⟦⊕⟧ i₂))
+                    (⟦⊕⟧-commute (X.fₒ′ s₁ ⟦⊕⟧ Y.fₒ′ s₂) (i₁ ⟦⊕⟧ i₂)))) ⟨
+          X⊗Y.fₛ′ (⟦ F.₁ (fᵢ ×₁ gᵢ) ⟧
+              ((⟦ F.₁ (S.π₁ ×₁ S.π₁) ⟧ ((X.fₒ′ s₁ ⟦⊕⟧ Y.fₒ′ s₂) ⟦⊕⟧ (i₁ ⟦⊕⟧ i₂))) ⟦⊕⟧
+               (⟦ F.₁ (S.π₂ ×₁ S.π₂) ⟧ ((X.fₒ′ s₁ ⟦⊕⟧ Y.fₒ′ s₂) ⟦⊕⟧ (i₁ ⟦⊕⟧ i₂))))) (s₁ , s₂)
+              ≈⟨ cong X⊗Y.fₛ (⟦⟧-cong (F.₁ (fᵢ ×₁ gᵢ)) (⟨⟩-⟦⊕⟧ ((X.fₒ′ s₁ ⟦⊕⟧ Y.fₒ′ s₂) ⟦⊕⟧ (i₁ ⟦⊕⟧ i₂)))) ⟨
+          X⊗Y.fₛ′ (⟦ F.₁ (fᵢ ×₁ gᵢ) ⟧ (⟦ F.₁ σ₂₃ ⟧ ((X.fₒ′ s₁ ⟦⊕⟧ Y.fₒ′ s₂) ⟦⊕⟧ (i₁ ⟦⊕⟧ i₂)))) (s₁ , s₂)
+              ≈⟨ cong X⊗Y.fₛ (F.homomorphism ((X.fₒ′ s₁ ⟦⊕⟧ Y.fₒ′ s₂) ⟦⊕⟧ (i₁ ⟦⊕⟧ i₂))) ⟨
+          X⊗Y.fₛ′ (⟦ F.₁ (fᵢ ×₁ gᵢ ∘ σ₂₃) ⟧ (_ ⟦⊕⟧ (i₁ ⟦⊕⟧ i₂))) (s₁ , s₂)
+              ≈⟨ cong X⊗Y.fₛ (⟦⟧-cong (F.₁ (fᵢ ×₁ gᵢ ∘ σ₂₃)) (⟦⊕⟧-congˡ (F.×-iso.isoˡ A′ C′ i))) ⟩
+          X⊗Y.fₛ′ (⟦ F.₁ (fᵢ ×₁ gᵢ ∘ σ₂₃) ⟧ ((X.fₒ′ s₁ ⟦⊕⟧ Y.fₒ′ s₂) ⟦⊕⟧ i)) (s₁ , s₂)
+              ∎
+        where
+          i₁ : Carrier (F.₀ A′)
+          i₁ = proj₁ (⟦ F.×-iso.from A′ C′ ⟧ i)
+          i₂ : Carrier (F.₀ C′)
+          i₂ = proj₂ (⟦ F.×-iso.from A′ C′ ⟧ i)
+      ≗-fₒ
+          : fₒ′ (×-System (wire fᵢ fₒ X) (wire gᵢ gₒ Y)) (s₁ , s₂)
+          B⊗D.≈ fₒ′ (wire (fᵢ ×₁ gᵢ ∘ σ₂₃) (fₒ ×₁ gₒ) (×-System X Y)) (s₁ , s₂)
+      ≗-fₒ = let open ≈-Reasoning B⊗D.setoid in begin
+          ⟦ F.₁ fₒ ⟧ (X.fₒ′ s₁) ⟦⊕⟧ ⟦ F.₁ gₒ ⟧ (Y.fₒ′ s₂) ≈⟨ ⟦⊕⟧-commute (X.fₒ′ s₁) (Y.fₒ′ s₂) ⟨
+          ⟦ F.₁ (fₒ ×₁ gₒ) ⟧ (X.fₒ′ s₁ ⟦⊕⟧ Y.fₒ′ s₂)      ∎
+
+commute
+    : {A B C D : Box}
+      (f : WiringDiagram A C)
+      (g : WiringDiagram B D)
+      (let fᵢ = WiringDiagram.input f)
+      (let gᵢ = WiringDiagram.input g)
+      (let fₒ = WiringDiagram.output f)
+      (let gₒ = WiringDiagram.output g)
+    → η C D ∘F (Wire fᵢ fₒ ∘F πˡ ※ Wire gᵢ gₒ ∘F πʳ)
+    ≃ Wire (fᵢ ×₁ gᵢ ∘ σ₂₃) (fₒ ×₁ gₒ) ∘F η A B
+commute f g =
+    pointwise-iso
+      (λ (X , Y) → mk-≅ (≅.refl (Setoids c c)) (λ i s → Commute.≗-fₛ f g X Y s i) (Commute.≗-fₒ f g X Y))
+      (λ { {X , Y} {X′ , Y′} (h , i) → S.refl X′ , S.refl Y′ })
+  where
+    open System
+
+⊗-homo : NaturalTransformation (Cats-C.-×- ∘F (Sys ⁂ Sys)) (Sys ∘F -⊞-)
+⊗-homo = ntHelper record
+    { η = λ (X , Y) → η X Y
+    ; commute = λ { {A , B} {C , D} (f , g) → commute f g }
+    }
+
+module Associativity
+  {A A′ B B′ C C′ : Obj}
+  (X : System (setoid (F.₀ A)) (F.₀ A′))
+  (Y : System (setoid (F.₀ B)) (F.₀ B′))
+  (Z : System (setoid (F.₀ C)) (F.₀ C′)) where
+
+  module X = System X
+  module Y = System Y
+  module Z = System Z
+
+  module X⊗Y = System (×-System X Y)
+  module [X⊗Y]⊗Z = System (×-System (×-System X Y) Z)
+  module X⊗[Y⊗Z] = System (×-System X (×-System Y Z))
+
+  open System
+
+  module _ (s : ∣ (X.S ×ₛ Y.S) ×ₛ Z.S ∣) where
+    open Setoid X⊗[Y⊗Z].S using (_≈_)
+
+    s₁ : ∣ X.S ∣
+    s₁ = proj₁ (proj₁ s)
+    s₂ : ∣ Y.S ∣
+    s₂ = proj₂ (proj₁ s)
+    s₃ : ∣ Z.S ∣
+    s₃ = proj₂ s
+
+    ≗-fₛ
+        : (i : Carrier (F.₀ (A ⊕ (B ⊕ C))))
+        → assocˡ {X.S} {Y.S} {Z.S} ⟨$⟩ System.fₛ′ (wire (S.assocʳ ∘ S.π₂) S.assocˡ (×-System (×-System X Y) Z)) i s
+        ≈ X⊗[Y⊗Z].fₛ′ i (assocˡ {X.S} {Y.S} {Z.S} ⟨$⟩ s)
+    ≗-fₛ i = begin
+        assocˡ ⟨$⟩ [X⊗Y]⊗Z.fₛ′ (⟦ F.₁ (S.assocʳ ∘ S.π₂) ⟧ ([X⊗Y]⊗Z.fₒ′ ((s₁ , s₂) , s₃) ⟦⊕⟧ i)) ((s₁ , s₂) , s₃)
+            ≈⟨ cong (assocˡ {X.S} {Y.S} {Z.S}) (cong [X⊗Y]⊗Z.fₛ (F.homomorphism ([X⊗Y]⊗Z.fₒ′ ((s₁ , s₂) , s₃) ⟦⊕⟧ i))) ⟩
+        assocˡ ⟨$⟩ [X⊗Y]⊗Z.fₛ′ (⟦ F.₁ S.assocʳ ⟧ (⟦ F.₁ S.π₂ ⟧ ([X⊗Y]⊗Z.fₒ′ ((s₁ , s₂) , s₃) ⟦⊕⟧ i))) ((s₁ , s₂) , s₃)
+            ≈⟨ cong (assocˡ {X.S} {Y.S} {Z.S}) (cong [X⊗Y]⊗Z.fₛ (⟦⟧-cong (F.₁ S.assocʳ) (F.F-resp-×.project₂ ([X⊗Y]⊗Z.fₒ′ ((s₁ , s₂) , s₃) , i)))) ⟩
+        assocˡ ⟨$⟩ [X⊗Y]⊗Z.fₛ′ (⟦ F.₁ S.assocʳ ⟧ i) ((s₁ , s₂) , s₃)
+            ≈⟨ cong (assocˡ {X.S} {Y.S} {Z.S}) (cong [X⊗Y]⊗Z.fₛ (⟦⟧-cong (F.₁ S.assocʳ) (F.×-iso.isoˡ A (B ⊕ C) i))) ⟨
+        assocˡ ⟨$⟩ [X⊗Y]⊗Z.fₛ′ (⟦ F.₁ S.assocʳ ⟧ (i₁ ⟦⊕⟧ i₂₃)) ((s₁ , s₂) , s₃)
+            ≈⟨ cong (assocˡ {X.S} {Y.S} {Z.S}) (cong [X⊗Y]⊗Z.fₛ (⟦⟧-cong (F.₁ S.assocʳ) (⟦⊕⟧-congˡ (F.×-iso.isoˡ B C i₂₃)))) ⟨
+        assocˡ ⟨$⟩ [X⊗Y]⊗Z.fₛ′ (⟦ F.₁ S.assocʳ ⟧ (i₁ ⟦⊕⟧ (i₂ ⟦⊕⟧ i₃))) ((s₁ , s₂) , s₃)
+            ≈⟨ cong (assocˡ {X.S} {Y.S} {Z.S}) (cong [X⊗Y]⊗Z.fₛ (⟦⊕⟧-assocʳ i₁ i₂ i₃)) ⟩
+        assocˡ ⟨$⟩ [X⊗Y]⊗Z.fₛ′ ((i₁ ⟦⊕⟧ i₂) ⟦⊕⟧ i₃) ((s₁ , s₂) , s₃)
+            ≈⟨ cong (assocˡ {X.S} {Y.S} {Z.S}) (cong (λg (< eval ∙ (X⊗Y.fₛ ∙ proj₁ₛ) ×-function proj₁ₛ , eval ∙ (Z.fₛ ∙ proj₂ₛ) ×-function proj₂ₛ >ₛ))
+                  (F.×-iso.isoʳ (A ⊕ B) C ((i₁ ⟦⊕⟧ i₂) , i₃))) ⟩
+        assocˡ ⟨$⟩ (X⊗Y.fₛ′ (i₁ ⟦⊕⟧ i₂) (s₁ , s₂) , Z.fₛ′ i₃ s₃)
+            ≈⟨ cong (assocˡ {X.S} {Y.S} {Z.S})
+                ((cong (λg (< eval ∙ (X.fₛ ∙ proj₁ₛ) ×-function proj₁ₛ , eval ∙ (Y.fₛ ∙ proj₂ₛ) ×-function proj₂ₛ >ₛ))
+                  (F.×-iso.isoʳ A B (i₁ , i₂))) , Z.S.refl) ⟩
+        X.fₛ′ i₁ s₁ , (Y.fₛ′ i₂ s₂ , Z.fₛ′ i₃ s₃)
+            ∎
+      where
+        open Setoids-CC using (λg; eval)
+        open ≈-Reasoning X⊗[Y⊗Z].S
+        open Func using (cong)
+        i₁ : Carrier (F.₀ A)
+        i₁ = proj₁ (⟦ F.×-iso.from A (B ⊕ C) ⟧ i)
+        i₂₃ : Carrier (F.₀ (B ⊕ C))
+        i₂₃ = proj₂ (⟦ F.×-iso.from A (B ⊕ C) ⟧ i)
+        i₂ : Carrier (F.₀ B)
+        i₂ = proj₁ (⟦ F.×-iso.from B C ⟧ i₂₃)
+        i₃ : Carrier (F.₀ C)
+        i₃ = proj₂ (⟦ F.×-iso.from B C ⟧ i₂₃)
+    module A⊗B⊗C = CommutativeMonoid (F.₀ (A′ ⊕ (B′ ⊕ C′)))
+    ≗-fₒ
+        : fₒ′ (wire (S.assocʳ ∘ S.π₂) S.assocˡ (×-System (×-System X Y) Z)) ((s₁ , s₂) , s₃)
+        A⊗B⊗C.≈ fₒ′ (×-System X (×-System Y Z)) (s₁ , (s₂ , s₃))
+    ≗-fₒ = begin
+        ⟦ F.₁ S.assocˡ ⟧ ((X.fₒ′ s₁ ⟦⊕⟧ Y.fₒ′ s₂) ⟦⊕⟧ Z.fₒ′ s₃) ≈⟨ ⟦⊕⟧-assocˡ (X.fₒ′ s₁) (Y.fₒ′ s₂) (Z.fₒ′ s₃) ⟩
+        X.fₒ′ s₁ ⟦⊕⟧ (Y.fₒ′ s₂ ⟦⊕⟧ Z.fₒ′ s₃)                    ∎
+      where
+        open ≈-Reasoning A⊗B⊗C.setoid
+
+associativity
+    : {A B C : Box}
+    → Wire (S.assocʳ ∘ S.π₂) S.assocˡ ∘F η (A ⊞ B) C ∘F (η A B ∘F πˡ ※ IdF ∘F πʳ)
+    ≃ η A (B ⊞ C) ∘F (IdF ∘F πˡ ※ η B C ∘F πʳ) ∘F (πˡ ∘F πˡ ※ πʳ ∘F πˡ ※ πʳ)
+associativity =
+    pointwise-iso
+      (λ { ((X , Y) , Z) → mk-≅ (≅.sym _ ×-assoc) (λ { i s → ≗-fₛ X Y Z s i }) λ { s → ≗-fₒ X Y Z s } })
+      (λ { {(X , Y) , Z} {(X′ , Y′) , Z′} ((h , i) , j) → S.refl X′ , S.refl Y′ , S.refl Z′ })
+  where
+    open Associativity
+    open System using (S)
+
+module Unitary {A B : Obj} (X : System (setoid (F.₀ A)) (F.₀ B)) where
+
+  module X = System X
+  module ⊤⊗X = System (×-System (discrete (setoid (F.₀ S.𝟘)) (F.₀ S.𝟘)) X)
+  module X⊗⊤ = System (×-System X (discrete (setoid (F.₀ S.𝟘)) (F.₀ S.𝟘)))
+  open System
+
+  module B = CommutativeMonoid (F.₀ B)
+
+  unitorˡ-≗fₛ
+      : (i : Carrier (F.₀ A))
+        (s : ∣ X.S ∣)
+      → proj₂ (System.fₛ′ (wire (S.i₂ ∘ S.π₂) (S.π₂ {S.𝟘} {B}) (×-System (discrete (setoid (F.₀ S.𝟘)) (F.₀ S.𝟘)) X)) i (tt , s))
+      X.S.≈ X.fₛ′ i s
+  unitorˡ-≗fₛ i s = begin
+      X.fₛ′ (⟦ F.₁ S.π₂ ⟧ (⟦ F.₁ (S.i₂ ∘ S.π₂) ⟧ (⊤⊗X.fₒ′ (tt , s) ⟦⊕⟧ i))) s       ≈⟨ cong X.fₛ (⟦⟧-cong (F.₁ S.π₂) (F.homomorphism (⊤⊗X.fₒ′ (tt , s) ⟦⊕⟧ i))) ⟩
+      X.fₛ′ (⟦ F.₁ S.π₂ ⟧ (⟦ F.₁ S.i₂ ⟧ (⟦ F.₁ S.π₂ ⟧ (⊤⊗X.fₒ′ (tt , s) ⟦⊕⟧ i)))) s ≈⟨ cong X.fₛ (⟦⟧-cong (F.₁ S.π₂) (⟦⟧-cong (F.₁ S.i₂) (F.F-resp-×.project₂ ((⊤⊗X.fₒ′ (tt , s) , i))))) ⟩
+      X.fₛ′ (⟦ F.₁ S.π₂ ⟧ (⟦ F.₁ S.i₂ ⟧ i)) s                                       ≈⟨ cong X.fₛ (F.homomorphism i) ⟨
+      X.fₛ′ (⟦ F.₁ (S.π₂ ∘ S.i₂) ⟧ i) s                                             ≈⟨ cong X.fₛ (F.F-resp-≈ S.π₂∘i₂≈id i) ⟩
+      X.fₛ′ (⟦ F.₁ _ ⟧ i) s                                                         ≈⟨ cong X.fₛ (F.identity i) ⟩
+      X.fₛ′ i s                                                                     ∎
+    where
+      open ≈-Reasoning X.S
+      open Func using (cong)
+
+  unitorˡ-≗fₒ
+      : (s : ∣ X.S ∣)
+      → fₒ′ (wire (S.i₂ ∘ S.π₂) S.π₂ (×-System (discrete (setoid (F.₀ S.𝟘)) (F.₀ S.𝟘)) X)) (tt , s) B.≈ X.fₒ′ s
+  unitorˡ-≗fₒ s = begin
+      ⟦ F.₁ S.π₂ ⟧ (_ ⟦⊕⟧ X.fₒ′ s)  ≈⟨ F.F-resp-×.project₂ (CommutativeMonoid.ε (F.₀ S.𝟘) , X.fₒ′ s) ⟩
+      X.fₒ′ s                       ∎
+    where
+      open ≈-Reasoning B.setoid
+
+  unitorʳ-≗fₛ
+      : (i : Carrier (F.₀ A))
+        (s : ∣ X.S ∣)
+      → proj₁ (System.fₛ′ (wire (S.i₁ ∘ S.π₂) (S.π₁ {B} {S.𝟘}) (×-System X (discrete (setoid (F.₀ S.𝟘)) (F.₀ S.𝟘)))) i (s , tt))
+      X.S.≈ X.fₛ′ i s
+  unitorʳ-≗fₛ i s = begin
+      X.fₛ′ (⟦ F.₁ S.π₁ ⟧ (⟦ F.₁ (S.i₁ ∘ S.π₂) ⟧ (X⊗⊤.fₒ′ (s , tt) ⟦⊕⟧ i))) s ≈⟨ cong X.fₛ (⟦⟧-cong (F.₁ S.π₁) (F.homomorphism (X⊗⊤.fₒ′ (s , tt) ⟦⊕⟧ i))) ⟩
+      X.fₛ′ (⟦ F.₁ _ ⟧ (⟦ F.₁ _ ⟧ (⟦ F.₁ S.π₂ ⟧ (_ ⟦⊕⟧ i)))) s                ≈⟨ cong X.fₛ (⟦⟧-cong (F.₁ S.π₁) (⟦⟧-cong (F.₁ S.i₁) (F.F-resp-×.project₂ (_ , i)))) ⟩
+      X.fₛ′ (⟦ F.₁ S.π₁ ⟧ (⟦ F.₁ S.i₁ ⟧ i)) s                                 ≈⟨ cong X.fₛ (F.homomorphism i) ⟨
+      X.fₛ′ (⟦ F.₁ (S.π₁ ∘ S.i₁) ⟧ i) s                                       ≈⟨ cong X.fₛ (F.F-resp-≈ S.π₁∘i₁≈id i) ⟩
+      X.fₛ′ (⟦ F.₁ _ ⟧ i) s                                                   ≈⟨ cong X.fₛ (F.identity i) ⟩
+      X.fₛ′ i s                                                               ∎
+    where
+      open ≈-Reasoning X.S
+      open Func using (cong)
+
+  unitorʳ-≗fₒ
+      : (s : ∣ X.S ∣)
+      → fₒ′ (wire (S.i₁ ∘ S.π₂) S.π₁ (×-System X (discrete (setoid (F.₀ S.𝟘)) (F.₀ S.𝟘)))) (s , tt) B.≈ X.fₒ′ s
+  unitorʳ-≗fₒ s = begin
+      ⟦ F.₁ S.π₁ ⟧ (X.fₒ′ s ⟦⊕⟧ _)  ≈⟨ F.F-resp-×.project₁ (X.fₒ′ s , CommutativeMonoid.ε (F.₀ S.𝟘)) ⟩
+      X.fₒ′ s                       ∎
+    where
+      open ≈-Reasoning B.setoid
+
+unitaryˡ
+    : {X : Box}
+    → Wire (S.i₂ ∘ S.π₂) S.π₂ ∘F η (S.𝟘 □ S.𝟘) X ∘F (ε ∘F πˡ ※ IdF ∘F πʳ) ≃ πʳ
+unitaryˡ =
+    pointwise-iso
+      (λ (_ , X) →
+        mk-≅
+          ⊤×A≅A
+          (λ i (_ , s) → unitorˡ-≗fₛ X i s)
+          (λ (_ , s) → unitorˡ-≗fₒ X s))
+      λ { {_} {_ , B} _ → S.refl B }
+    where
+      open Unitary
+      open CartesianMonoidal Setoids-CC.cartesian using (⊤×A≅A)
+      open System using (module S)
+
+unitaryʳ
+    : {X : Box}
+    → Wire (S.i₁ ∘ S.π₂) S.π₁ ∘F η X (S.𝟘 □ S.𝟘) ∘F (IdF ∘F πˡ ※ ε ∘F πʳ) ≃ πˡ
+unitaryʳ =
+    pointwise-iso
+      (λ (X , _) →
+        mk-≅
+          A×⊤≅A
+          (λ i (s , _) → unitorʳ-≗fₛ X i s)
+          (λ (s , _) → unitorʳ-≗fₒ X s))
+      λ { {_} {B , _} _ → S.refl B }
+    where
+      open Unitary
+      open CartesianMonoidal Setoids-CC.cartesian using (A×⊤≅A)
+      open System using (module S)
+
+Sys-IsMF : IsMonoidalFunctor DWD-MC Cats-MC Sys
+Sys-IsMF = record
+    { ε = ε
+    ; ⊗-homo = ⊗-homo
+    ; associativity = associativity
+    ; unitaryˡ = unitaryˡ
+    ; unitaryʳ = unitaryʳ
+    }
+
+Sys-MF : MonoidalFunctor DWD-MC Cats-MC
+Sys-MF = record
+  { F = Sys
+  ; isMonoidal = Sys-IsMF
+  }