{-# OPTIONS --without-K --safe #-}

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.Instance.WiringDiagram.System
    {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 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)
open import Categories.Category.Monoidal.Utilities using (module Shorthands)
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)
open import Data.Product using (_,_)
open import Data.Product.Function.NonDependent.Setoid using (_×-function_; proj₁ₛ; proj₂ₛ; swapₛ)
open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_)
open import Data.Setoid using (_⇒ₛ_; ∣_∣)
open import Data.Setoid.Unit using (⊤ₛ)
open import Data.System using (System; _≤_; Systems[_,_]; Systems-SMC; discrete)
open import Data.Unit.Polymorphic using (tt)
open import Data.WiringDiagram.Core S.semiadditiveDagger using (Box; WiringDiagram; _□_; _⧈_; _⌻_; _≈-⧈_)
open import Data.WiringDiagram.Directed S.semiadditiveDagger using (DWD; Pulsh)
open import Function using (Func; _⟶ₛ_; _⟨$⟩_; id; _$_)
open import Function.Construct.Identity using () renaming (function to Id)
open import Function.Construct.Setoid using (_∙_)

module F = CartesianF F

module 𝒞 = Category 𝒞

open Box
open CMonoidHomomorphism
open Category 𝒞 using (Obj; _⇒_; _∘_)
open CommutativeMonoid using (setoid; Carrier; refl; sym)
open Func
open IdempotentSemiadditiveDagger S using (_⊕_; _×₁_)
open WiringDiagram using (input; output)

_⟦⊕⟧_ : {A B : Obj} → Carrier (F.₀ A) → Carrier (F.₀ B) → Carrier (F.₀ (A ⊕ B))
_⟦⊕⟧_ {A} {B} a b = ⟦ F.×-iso.to A B ⟧ (a , b)

⟦⊕⟧-cong
    : {A B : Obj}
      (let module FA = CommutativeMonoid (F.₀ A))
      (let module FB = CommutativeMonoid (F.₀ B))
      (let module F[A+B] = CommutativeMonoid (F.₀ (A ⊕ B)))
      {a a′ : Carrier (F.₀ A)}
      {b b′ : Carrier (F.₀ B)}
    → a FA.≈ a′
    → b FB.≈ b′
    → a ⟦⊕⟧ b F[A+B].≈ a′ ⟦⊕⟧ b′
⟦⊕⟧-cong {A} {B} ≈a ≈b = ⟦⟧-cong (F.×-iso.to A B) (≈a , ≈b)

⟦⊕⟧-commute
    : {A B C D : Obj}
      {f : A ⇒ B}
      {g : C ⇒ D}
      (a : Carrier (F.₀ A))
      (c : Carrier (F.₀ C))
    → (let open CommutativeMonoid (F.₀ (B ⊕ D)) using (_≈_))
    → ⟦ F.₁ (f ×₁ g) ⟧ (a ⟦⊕⟧ c) ≈ ⟦ F.₁ f ⟧ a ⟦⊕⟧ ⟦ F.₁ g ⟧ c
⟦⊕⟧-commute {A} {B} {C} {D} {f} {g} a c- = begin
    ⟦ F.₁ (f ×₁ g) ⟧ (a ⟦⊕⟧ c-)   ≈⟨ ⊗-F.⊗-homo.sym-commute (f , g) (a , c-) ⟩
    ⟦ F.₁ f ⟧ a ⟦⊕⟧ ⟦ F.₁ g ⟧ c-  ∎
  where
    open ≈-Reasoning (setoid (F.₀ (B ⊕ D)))
    open CommutativeMonoid (F.₀ (B ⊕ D)) using (_≈_)
    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-) ≈⟨ ⊗-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))
      (let module F[A+B] = CommutativeMonoid (F.₀ (A ⊕ B)))
      {a : Carrier (F.₀ A)}
      {b b′ : Carrier (F.₀ B)}
    → b FB.≈ b′
    → a ⟦⊕⟧ b F[A+B].≈ a ⟦⊕⟧ b′
⟦⊕⟧-congˡ {A} ≈b = ⟦⊕⟧-cong (refl (F.₀ A)) ≈b


⟦⊕⟧-congʳ
    : {A B : Obj}
      (let module FA = CommutativeMonoid (F.₀ A))
      (let module F[A+B] = CommutativeMonoid (F.₀ (A ⊕ B)))
      {a a′ : Carrier (F.₀ A)}
      {b : Carrier (F.₀ B)}
    → a FA.≈ a′
    → a ⟦⊕⟧ b F[A+B].≈ a′ ⟦⊕⟧ b
⟦⊕⟧-congʳ {B = B} ≈a = ⟦⊕⟧-cong ≈a (refl (F.₀ B))

module _ {Aᵢ Aₒ Bᵢ Bₒ : Obj} (i : Aₒ ⊕ Bᵢ ⇒ Aᵢ) (o : Aₒ ⇒ Bₒ) where

  A-System B-System : Set (suc c)
  A-System = System (setoid (F.₀ Aᵢ)) (F.₀ Aₒ)
  B-System = System (setoid (F.₀ Bᵢ)) (F.₀ Bₒ)

  A-Systems B-Systems : Category (suc c) c c
  A-Systems = Systems[ setoid (F.₀ Aᵢ) , F.₀ Aₒ ]
  B-Systems = Systems[ setoid (F.₀ Bᵢ) , F.₀ Bₒ ]

  I⇒ : CMonoidHomomorphism c c (F.₀ (Aₒ ⊕ Bᵢ)) (F.₀ Aᵢ)
  I⇒ = F.₁ i

  O⇒ : CMonoidHomomorphism c c (F.₀ Aₒ) (F.₀ Bₒ)
  O⇒ = F.₁ o

  wire : A-System → B-System
  wire sys = record
      { S = X.S
      ; fₛ = λg (eval ∙ (X.fₛ ×-function Id X.S) ∙ ⟨ func I⇒ ∙ func (F.×-iso.to Aₒ Bᵢ) ∙ X.fₒ ×-function Id (setoid (F.₀ Bᵢ)) ∙ swapₛ , π₂ ⟩)
      ; fₒ = func O⇒ ∙ X.fₒ
      }
    where
      module X = System sys
      open CartesianClosed (Setoids-CCC c) using (λg; eval; cartesian)
      open Cartesian cartesian using (π₁; π₂; ⟨_,_⟩)

  wire-≤ : {A B : A-System} → A ≤ B → wire A ≤ wire B
  wire-≤ {A} {B} A≤B = record
      { ⇒S = ⇒S
      ; ≗-fₛ = ≗-wfₛ
      ; ≗-fₒ = ≗-wfₒ
      }
    where
      module A = System A
      module B = System B
      module wA = System (wire A)
      module wB = System (wire B)
      open System
      open _≤_ A≤B
      ≗-wfₛ
          : (i : Carrier (F.₀ Bᵢ))
            (s : ∣ wA.S ∣)
          → ⇒S ⟨$⟩ wA.fₛ′ i s B.S.≈ wB.fₛ′ i (⇒S ⟨$⟩ s)
      ≗-wfₛ i s = begin
          ⇒S ⟨$⟩ A.fₛ′ (⟦ I⇒ ⟧ (A.fₒ′ s ⟦⊕⟧ i)) s             ≈⟨ ≗-fₛ (⟦ I⇒ ⟧ (A.fₒ′ s ⟦⊕⟧ i)) s ⟩
          B.fₛ′ (⟦ I⇒ ⟧ (A.fₒ′ s ⟦⊕⟧ i)) (⇒S ⟨$⟩ s)           ≈⟨ cong B.fₛ (⟦⟧-cong I⇒ (⟦⊕⟧-congʳ (≗-fₒ s))) ⟩
          B.fₛ′ (⟦ I⇒ ⟧ (B.fₒ′ (⇒S ⟨$⟩ s) ⟦⊕⟧ i)) (⇒S ⟨$⟩ s)  ∎
        where
          open ≈-Reasoning B.S
      ≗-wfₒ
          : (s : ∣ wA.S ∣)
          → (open CommutativeMonoid (F.₀ Bₒ) using (_≈_))
          → wA.fₒ′ s ≈ wB.fₒ′ (⇒S ⟨$⟩ s)
      ≗-wfₒ s = ⟦⟧-cong O⇒ (≗-fₒ s)

  Wire : Functor A-Systems B-Systems
  Wire = record
      { F₀ = wire
      ; F₁ = wire-≤
      ; identity = λ {X} → System.S.refl X
      ; homomorphism = λ {Z = Z} → System.S.refl Z
      ; F-resp-≈ = id
      }

identity : {Aᵢ Aₒ : Obj} → Wire {Aᵢ} {Aₒ} S.π₂ 𝒞.id ≃ IdF
identity {Aᵢ} {Aₒ} = niHelper record
    { η = ≤X
    ; η⁻¹ = ≥X
    ; commute = λ {_ Y} _ → System.S.refl Y
    ; iso = λ X → record
        { isoˡ = System.S.refl X
        ; isoʳ = System.S.refl X
        }
    }
  where
    module _ (X : System (setoid (F.₀ Aᵢ)) (F.₀ Aₒ)) where
      module X = System X
      open IsProduct F.F-resp-× using (project₂)
      ≤X : wire S.π₂ 𝒞.id X ≤ X
      ≤X = record
          { ⇒S = Id X.S
          ; ≗-fₛ = λ i s → cong X.fₛ (project₂ (X.fₒ′ s , i))
          ; ≗-fₒ = λ s → F.identity (X.fₒ′ s)
          }
      ≥X : X ≤ wire S.π₂ 𝒞.id X
      ≥X = record
          { ⇒S = Id X.S
          ; ≗-fₛ = λ i s → X.S.sym (cong X.fₛ (project₂ (X.fₒ′ s , i)))
          ; ≗-fₒ = λ s → sym (F.₀ Aₒ) (F.identity (X.fₒ′ s))
          }

homomorphism
    : {Xᵢ Xₒ Yᵢ Yₒ Zᵢ Zₒ : Obj}
      {fᵢ : Xₒ ⊕ Yᵢ ⇒ Xᵢ}
      {fₒ : Xₒ ⇒ Yₒ}
      {gᵢ : Yₒ ⊕ Zᵢ ⇒ Yᵢ}
      {gₒ : Yₒ ⇒ Zₒ}
    → Wire (input ((gᵢ ⧈ gₒ) ⌻ (fᵢ ⧈ fₒ))) (output ((gᵢ ⧈ gₒ) ⌻ (fᵢ ⧈ fₒ)))
    ≃ Wire gᵢ gₒ ∘F Wire fᵢ fₒ
homomorphism {Xᵢ} {Xₒ} {Yᵢ} {Yₒ} {Zᵢ} {Zₒ} {fᵢ} {fₒ} {gᵢ} {gₒ} = niHelper record
    { η = η
    ; η⁻¹ = η⁻¹
    ; commute = λ {_ Y} _ → System.S.refl Y
    ; iso = λ X → record
        { isoˡ = System.S.refl X
        ; isoʳ = System.S.refl X
        }
    }
  where
    module _ (X : System (setoid (F.₀ Xᵢ)) (F.₀ Xₒ)) where
      module X = System X
      module _ (i : Carrier (F.₀ Zᵢ)) (s : ∣ X.S ∣) where
        lem₁
            : (let open CommutativeMonoid (F.₀ Yᵢ) using (_≈_))
            → ⟦ F.₁ (gᵢ ∘ fₒ ×₁ 𝒞.id) ⟧ (X.fₒ′ s ⟦⊕⟧ i) ≈ ⟦ F.₁ gᵢ ⟧ (⟦ F.₁ fₒ ⟧ (X.fₒ′ s) ⟦⊕⟧ i)
        lem₁ = begin
            ⟦ F.₁ (gᵢ ∘ fₒ ×₁ 𝒞.id) ⟧ (X.fₒ′ s ⟦⊕⟧ i)             ≈⟨ F.homomorphism (X.fₒ′ s ⟦⊕⟧ i) ⟩
            ⟦ F.₁ gᵢ ⟧ (⟦ F.₁ (fₒ ×₁ 𝒞.id) ⟧ (X.fₒ′ s ⟦⊕⟧ i))     ≈⟨ ⟦⟧-cong (F.₁ gᵢ) (⟦⊕⟧-commute (X.fₒ′ s) i) ⟩
            ⟦ F.₁ gᵢ ⟧ (⟦ F.₁ fₒ ⟧ (X.fₒ′ s) ⟦⊕⟧ ⟦ F.₁ 𝒞.id ⟧ i)  ≈⟨ ⟦⟧-cong (F.₁ gᵢ) (⟦⊕⟧-congˡ (F.identity i)) ⟩
            ⟦ F.₁ gᵢ ⟧ (⟦ F.₁ fₒ ⟧ (X.fₒ′ s) ⟦⊕⟧ i)               ∎
          where
            open ≈-Reasoning (setoid (F.₀ Yᵢ))
        lem₂
            : (let open CommutativeMonoid (F.₀ (Xₒ ⊕ (Xₒ ⊕ Zᵢ))) using (_≈_))
            → ⟦ 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)       ≈⟨ ⟨⟩-⟦⊕⟧ (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
            open ≈-Reasoning (setoid (F.₀ (Xₒ ⊕ (Xₒ ⊕ Zᵢ))))
        lem₃
            : (let open CommutativeMonoid (F.₀ (Xₒ ⊕ Yᵢ)) using (_≈_))
            → ⟦ F.₁ S.⟨ S.π₁ , gᵢ ∘ fₒ ×₁ 𝒞.id ⟩ ⟧ (X.fₒ′ s ⟦⊕⟧ i)
            ≈ (X.fₒ′ s ⟦⊕⟧ (⟦ F.₁ gᵢ ⟧ (⟦ F.₁ fₒ ⟧ (X.fₒ′ s) ⟦⊕⟧ i)))
        lem₃ = begin
            ⟦ F.₁ S.⟨ S.π₁ , gᵢ ∘ fₒ ×₁ 𝒞.id ⟩ ⟧ (X.fₒ′ s ⟦⊕⟧ i)                            ≈⟨ F.F-resp-≈ (S.⟨⟩-congˡ 𝒞.identityʳ) (X.fₒ′ s ⟦⊕⟧ i) ⟨
            ⟦ F.₁ S.⟨ S.π₁ , (gᵢ ∘ fₒ ×₁ 𝒞.id) ∘ 𝒞.id ⟩ ⟧ (X.fₒ′ s ⟦⊕⟧ i)                   ≈⟨ F.F-resp-≈ S.second∘⟨⟩ (X.fₒ′ s ⟦⊕⟧ i) ⟨
            ⟦ F.₁ (𝒞.id ×₁ (gᵢ ∘ fₒ ×₁ 𝒞.id) ∘ S.⟨ S.π₁ , 𝒞.id ⟩) ⟧ (X.fₒ′ s ⟦⊕⟧ i)         ≈⟨ F.homomorphism (X.fₒ′ s ⟦⊕⟧ i) ⟩
            ⟦ F.₁ (𝒞.id ×₁ (gᵢ ∘ fₒ ×₁ 𝒞.id)) ⟧ (⟦ F.₁ S.⟨ S.π₁ , 𝒞.id ⟩ ⟧ (X.fₒ′ s ⟦⊕⟧ i)) ≈⟨ ⟦⟧-cong (F.₁ (𝒞.id ×₁ (gᵢ ∘ fₒ ×₁ 𝒞.id))) lem₂ ⟩
            ⟦ F.₁ (𝒞.id ×₁ (gᵢ ∘ fₒ ×₁ 𝒞.id)) ⟧ (X.fₒ′ s ⟦⊕⟧ (X.fₒ′ s ⟦⊕⟧ i))               ≈⟨ ⟦⊕⟧-commute (X.fₒ′ s) (X.fₒ′ s ⟦⊕⟧ i) ⟩
            ⟦ F.₁ 𝒞.id ⟧ (X.fₒ′ s) ⟦⊕⟧ ⟦ F.₁ (gᵢ ∘ fₒ ×₁ 𝒞.id) ⟧ (X.fₒ′ s ⟦⊕⟧ i)            ≈⟨ ⟦⊕⟧-cong (F.identity (X.fₒ′ s)) lem₁ ⟩
            X.fₒ′ s ⟦⊕⟧ ⟦ F.₁ gᵢ ⟧ (⟦ F.₁ fₒ ⟧ (X.fₒ′ s) ⟦⊕⟧ i)                             ∎
          where
            open ≈-Reasoning (setoid (F.₀ (Xₒ ⊕ Yᵢ)))
        ≗-fₛ
            : X.fₛ′ (⟦ F.₁ (fᵢ ∘ S.⟨ S.π₁ , gᵢ ∘ fₒ ×₁ 𝒞.id ⟩) ⟧ (X.fₒ′ s ⟦⊕⟧ i)) s X.S.≈
              X.fₛ′ (⟦ F.₁ fᵢ ⟧ (X.fₒ′ s ⟦⊕⟧ (⟦ F.₁ gᵢ ⟧ (⟦ F.₁ fₒ ⟧ (X.fₒ′ s) ⟦⊕⟧ i)))) s
        ≗-fₛ = cong X.fₛ $ begin
            ⟦ F.₁ (fᵢ ∘ S.⟨ S.π₁ , gᵢ ∘ fₒ ×₁ 𝒞.id ⟩) ⟧ (X.fₒ′ s ⟦⊕⟧ i)       ≈⟨ F.homomorphism (X.fₒ′ s ⟦⊕⟧ i) ⟩
            ⟦ F.₁ fᵢ ⟧ (⟦ F.₁ S.⟨ S.π₁ , gᵢ ∘ fₒ ×₁ 𝒞.id ⟩ ⟧ (X.fₒ′ s ⟦⊕⟧ i)) ≈⟨ ⟦⟧-cong (F.₁ fᵢ) lem₃ ⟩
            ⟦ F.₁ fᵢ ⟧ (X.fₒ′ s ⟦⊕⟧ ⟦ F.₁ gᵢ ⟧ (⟦ F.₁ fₒ ⟧ (X.fₒ′ s) ⟦⊕⟧ i))  ∎
          where
            open ≈-Reasoning (setoid (F.₀ Xᵢ))
      η : wire (input ((gᵢ ⧈ gₒ) ⌻ (fᵢ ⧈ fₒ))) (output ((gᵢ ⧈ gₒ) ⌻ (fᵢ ⧈ fₒ))) X ≤ wire gᵢ gₒ (wire fᵢ fₒ X)
      η = record
          { ⇒S = Id X.S
          ; ≗-fₛ = ≗-fₛ
          ; ≗-fₒ = λ s → F.homomorphism (X.fₒ′ s)
          }
      η⁻¹ : wire gᵢ gₒ (wire fᵢ fₒ X) ≤ wire (input ((gᵢ ⧈ gₒ) ⌻ (fᵢ ⧈ fₒ))) (output ((gᵢ ⧈ gₒ) ⌻ (fᵢ ⧈ fₒ))) X
      η⁻¹ = record
          { ⇒S = Id X.S
          ; ≗-fₛ = λ i s → X.S.sym (≗-fₛ i s)
          ; ≗-fₒ = λ s → sym (F.₀ Zₒ) (F.homomorphism (X.fₒ′ s))
          }

Sys-resp-≈
    : {A B : Box}
      {f g : WiringDiagram A B}
    → f ≈-⧈ g
    → Wire (input f) (output f) ≃ Wire (input g) (output g)
Sys-resp-≈ {A} {B} {f} {g} f≈g = niHelper record
    { η = wf≤wg
    ; η⁻¹ = wg≤wf
    ; commute = λ {_ Y} _ → System.S.refl Y
    ; iso = λ X → record
        { isoˡ = System.S.refl X
        ; isoʳ = System.S.refl X
        }
    }
  where
    module A = Box A
    module B = Box B
    module _ (X : System (setoid (F.₀ A.ᵢ)) (F.₀ A.ₒ)) where

      fᵢ gᵢ : A.ₒ ⊕ B.ᵢ ⇒ A.ᵢ
      fᵢ = input f
      gᵢ = input g

      fₒ gₒ : A.ₒ ⇒ B.ₒ
      fₒ = output f
      gₒ = output g

      open _≈-⧈_ f≈g

      module X = System X

      wf≤wg : wire fᵢ fₒ X ≤ wire gᵢ gₒ X
      wf≤wg = record
          { ⇒S = Id X.S
          ; ≗-fₛ = λ i s → cong X.fₛ (F.F-resp-≈ ≈i (X.fₒ′ s ⟦⊕⟧ i))
          ; ≗-fₒ = λ s → F.F-resp-≈ ≈o (X.fₒ′ s)
          }

      wg≤wf : wire (input g) (output g) X ≤ wire (input f) (output f) X
      wg≤wf = record
          { ⇒S = Id X.S
          ; ≗-fₛ = λ i s → X.S.sym (cong X.fₛ (F.F-resp-≈ ≈i (X.fₒ′ s ⟦⊕⟧ i)))
          ; ≗-fₒ = λ s → sym (F.₀ B.ₒ) (F.F-resp-≈ ≈o (X.fₒ′ s))
          }

Sys : Functor DWD (Cats (suc c) c c)
Sys = record
    { F₀ = λ (i □ o) → Systems[ setoid (F.₀ i) , F.₀ o ]
    ; F₁ = λ (input ⧈ output) → Wire input output
    ; identity = identity
    ; homomorphism = homomorphism
    ; F-resp-≈ = Sys-resp-≈
    }

module Sys = Functor Sys