{-# 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
  }