From 9e2f3f3bb9916dca8d4ad4b162ce5b089c26b82e Mon Sep 17 00:00:00 2001 From: Jacques Comeaux Date: Mon, 13 Jul 2026 16:06:43 -0700 Subject: Construct Sys functor from wiring diagrams to Cats --- Functor/Instance/WiringDiagram/System.agda | 382 +++++++++++++++++++++++++++++ 1 file changed, 382 insertions(+) create mode 100644 Functor/Instance/WiringDiagram/System.agda (limited to 'Functor/Instance/WiringDiagram') diff --git a/Functor/Instance/WiringDiagram/System.agda b/Functor/Instance/WiringDiagram/System.agda new file mode 100644 index 0000000..753f0f0 --- /dev/null +++ b/Functor/Instance/WiringDiagram/System.agda @@ -0,0 +1,382 @@ +{-# OPTIONS --without-K --safe #-} + +open import Categories.Category using (Category) +open import Categories.Category.Cartesian.Bundle using (CartesianCategory) +open import Categories.Category.Cartesian.Monoidal using (module CartesianMonoidal) +open import Categories.Category.Cocartesian.Monoidal using (module CocartesianMonoidal) +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) + +open CartesianMonoidal using (monoidal) +open CocartesianMonoidal using (+-monoidal) + +module Functor.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 Data.System.Monoidal as Sys-⊗ +import Relation.Binary.Reasoning.Setoid as ≈-Reasoning + +open import Algebra using (CommutativeMonoid) +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.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 using (Box; WiringDiagram; _□_; _⧈_; _⌻_; _≈-⧈_) +open import Data.WiringDiagram.Directed S 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 Shorthands (+-monoidal S.cocartesian) using (α⇒) +open Shorthands (monoidal S.cartesian) using () renaming (α⇒ to α⇒′) +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.F-resp-≈ (S.×₁-⊕₁ f g) (a ⟦⊕⟧ c-) ⟨ + ⟦ 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 + open 𝒞-CC using (_×₁_) + ⊗-F : MonoidalFunctor 𝒞-CC.monoidalCategory (CMonoids-CC.monoidalCategory {c} {c}) + ⊗-F = isMonoidalFunctor {C = 𝒞-CC} {CMonoids-CC {c} {c}} F + module ⊗-F = MonoidalFunctor ⊗-F + +⟦△⟧ : {A : Obj} + (a : Carrier (F.₀ A)) + → (let open CommutativeMonoid (F.₀ (A ⊕₀ A)) using (_≈_)) + → ⟦ F.₁ △ ⟧ a ≈ a ⟦⊕⟧ a +⟦△⟧ {A} a = begin + ⟦ F.₁ △ ⟧ a ≈⟨ F.identity ((⟦ F.₁ △ ⟧ a)) ⟨ + ⟦ F.₁ 𝒞.id ⟧ (⟦ F.₁ △ ⟧ a) ≈⟨ F.F-resp-≈ ⊕.identity (⟦ F.₁ △ ⟧ a) ⟨ + ⟦ F.₁ (𝒞.id ⊕₁ 𝒞.id) ⟧ (⟦ F.₁ △ ⟧ a) ≈⟨ F.homomorphism a ⟨ + ⟦ F.₁ (𝒞.id ⊕₁ 𝒞.id ∘ △) ⟧ a ≈⟨ switch-fromtoˡ (F.×-iso A A) {h = F.₁ (𝒞.id ⊕₁ 𝒞.id ∘ △)} {k = CMonoids-CC.⟨ F.₁ 𝒞.id , F.₁ 𝒞.id ⟩} (F.F-resp-⟨⟩ 𝒞.id 𝒞.id) a ⟩ + ⟦ F.₁ 𝒞.id ⟧ a ⟦⊕⟧ ⟦ F.₁ 𝒞.id ⟧ a ≈⟨ ⟦⊕⟧-cong (F.identity a) (F.identity a) ⟩ + a ⟦⊕⟧ a ∎ + where + open ≈-Reasoning (setoid (F.₀ (A ⊕₀ A))) + open Product (F.F-prod A A) using (⟨⟩-cong₂) + module ⊕ = Functor S.⊕ + +⟦α⇒⟧ + : {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.₁ α⇒ ⟧ ((a ⟦⊕⟧ b) ⟦⊕⟧ c) ≈ a ⟦⊕⟧ (b ⟦⊕⟧ c) +⟦α⇒⟧ {A} {B} {C} a b c- = begin + ⟦ F.₁ α⇒ ⟧ ((a ⟦⊕⟧ b) ⟦⊕⟧ c-) ≈⟨ F.F-resp-≈ S.≈α⇒ ((a ⟦⊕⟧ b) ⟦⊕⟧ c-) ⟨ + ⟦ F.₁ α⇒′ ⟧ ((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 + +⟦⊕⟧-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.p₂ 𝒞.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.p₂ 𝒞.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.p₂ 𝒞.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.₁ (α⇒ 𝒞.∘ △ ⊕₁ 𝒞.id) ⟧ (X.fₒ′ s ⟦⊕⟧ i) + ≈ X.fₒ′ s ⟦⊕⟧ (X.fₒ′ s ⟦⊕⟧ i) + lem₂ = begin + ⟦ F.₁ (α⇒ 𝒞.∘ △ ⊕₁ 𝒞.id) ⟧ (X.fₒ′ s ⟦⊕⟧ i) ≈⟨ F.homomorphism (X.fₒ′ s ⟦⊕⟧ i) ⟩ + ⟦ F.₁ α⇒ ⟧ (⟦ F.₁ (△ ⊕₁ 𝒞.id) ⟧ (X.fₒ′ s ⟦⊕⟧ i)) ≈⟨ ⟦⟧-cong (F.₁ α⇒) (⟦⊕⟧-commute (X.fₒ′ s) i) ⟩ + ⟦ F.₁ α⇒ ⟧ (⟦ F.₁ △ ⟧ (X.fₒ′ s) ⟦⊕⟧ ⟦ F.₁ 𝒞.id ⟧ i) ≈⟨ ⟦⟧-cong (F.₁ α⇒) (⟦⊕⟧-cong (⟦△⟧ (X.fₒ′ s)) (F.identity i)) ⟩ + ⟦ F.₁ α⇒ ⟧ ((X.fₒ′ s ⟦⊕⟧ X.fₒ′ s) ⟦⊕⟧ i) ≈⟨ ⟦α⇒⟧ (X.fₒ′ s) (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.₁ (𝒞.id ⊕₁ (gᵢ ∘ fₒ ⊕₁ 𝒞.id) 𝒞.∘ α⇒ 𝒞.∘ △ ⊕₁ 𝒞.id) ⟧ (X.fₒ′ s ⟦⊕⟧ i) + ≈ (X.fₒ′ s ⟦⊕⟧ (⟦ F.₁ gᵢ ⟧ (⟦ F.₁ fₒ ⟧ (X.fₒ′ s) ⟦⊕⟧ i))) + lem₃ = begin + ⟦ F.₁ (𝒞.id ⊕₁ (gᵢ ∘ fₒ ⊕₁ 𝒞.id) 𝒞.∘ α⇒ 𝒞.∘ △ ⊕₁ 𝒞.id) ⟧ (X.fₒ′ s ⟦⊕⟧ i) ≈⟨ F.homomorphism (X.fₒ′ s ⟦⊕⟧ i) ⟩ + ⟦ F.₁ (𝒞.id ⊕₁ (gᵢ ∘ fₒ ⊕₁ 𝒞.id)) ⟧ (⟦ F.₁ (α⇒ 𝒞.∘ △ ⊕₁ 𝒞.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ᵢ ∘ 𝒞.id ⊕₁ (gᵢ ∘ fₒ ⊕₁ 𝒞.id) 𝒞.∘ α⇒ 𝒞.∘ △ ⊕₁ 𝒞.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ᵢ ∘ 𝒞.id ⊕₁ (gᵢ ∘ fₒ ⊕₁ 𝒞.id) 𝒞.∘ α⇒ 𝒞.∘ △ ⊕₁ 𝒞.id) ⟧ (X.fₒ′ s ⟦⊕⟧ i) ≈⟨ F.homomorphism (X.fₒ′ s ⟦⊕⟧ i) ⟩ + ⟦ F.₁ fᵢ ⟧ (⟦ F.₁ (𝒞.id ⊕₁ (gᵢ ∘ fₒ ⊕₁ 𝒞.id) 𝒞.∘ α⇒ 𝒞.∘ △ ⊕₁ 𝒞.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-≈ + } -- cgit v1.2.3