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 --- Category/Dagger/Semiadditive.agda | 27 +- Data/System.agda | 10 +- Functor/Instance/WiringDiagram/System.agda | 382 +++++++++++++++++++++++++++++ 3 files changed, 413 insertions(+), 6 deletions(-) create mode 100644 Functor/Instance/WiringDiagram/System.agda diff --git a/Category/Dagger/Semiadditive.agda b/Category/Dagger/Semiadditive.agda index a6a9e57..e8a9b39 100644 --- a/Category/Dagger/Semiadditive.agda +++ b/Category/Dagger/Semiadditive.agda @@ -10,6 +10,7 @@ import Categories.Morphism.Reasoning as β‡’-Reasoning open import Categories.Category.BinaryProducts π’ž using (BinaryProducts) open import Categories.Category.Cartesian π’ž using (Cartesian) +open import Categories.Category.Cartesian.Monoidal using (module CartesianMonoidal) open import Categories.Category.Cocartesian π’ž using (Cocartesian) open import Categories.Category.Cocartesian.Monoidal using (module CocartesianMonoidal) open import Categories.Category.Cocartesian.SymmetricMonoidal using (module CocartesianSymmetricMonoidal) @@ -54,7 +55,7 @@ record SemiadditiveDagger : Set (suc (o βŠ” β„“ βŠ” e)) where open Cocartesian cocartesian using ([]∘+-assocΚ³; []∘+-swap) renaming (_+_ to _βŠ•β‚€_; _+₁_ to infixr 10 _βŠ•β‚_; -+- to βŠ•) public open CocartesianMonoidal cocartesian using (+-monoidal) public open Cocartesian cocartesian using (i₁; iβ‚‚; Β‘) public - open Cocartesian cocartesian using (βŠ₯; [_,_]; ∘[]; []∘+₁; []-congβ‚‚; coproduct; Β‘-unique; inject₁; injectβ‚‚; +-unique; +-Ξ·) + open Cocartesian cocartesian using (βŠ₯; [_,_]; ∘[]; []∘+₁; []-congΛ‘; []-congβ‚‚; coproduct; Β‘-unique; inject₁; injectβ‚‚; +-unique; +-Ξ·) renaming (βˆ‡βˆ˜+₁ to β–½βˆ˜+₁) open CocartesianSymmetricMonoidal π’ž cocartesian using (+-symmetric) open HasDagger dagger using (_†; †-involutive; ⟨_βŸ©β€ ; †-identity; †-homomorphism) public open Monoidal +-monoidal using (unitorΛ‘-commute-from; unitorΚ³-commute-from; assoc-commute-from; module unitorΛ‘; module unitorΚ³; module associator) @@ -421,6 +422,30 @@ record SemiadditiveDagger : Set (suc (o βŠ” β„“ βŠ” e)) where ; products = products } + open Cartesian cartesian using (_×₁_) + open CartesianMonoidal cartesian using (monoidal) + open Shorthands monoidal using () renaming (Ξ±β‡’ to Ξ±β‡’β€²) + + ×₁-βŠ•β‚ : {A B C D : Obj} (f : A β‡’ B) (g : C β‡’ D) β†’ f ×₁ g β‰ˆ f βŠ•β‚ g + ×₁-βŠ•β‚ f g = begin + (f ∘ p₁) βŠ•β‚ (g ∘ pβ‚‚) ∘ β–³ β‰ˆβŸ¨ pushΛ‘ βŠ—-distrib-over-∘ ⟩ + f βŠ•β‚ g ∘ p₁ βŠ•β‚ pβ‚‚ ∘ β–³ β‰ˆβŸ¨ elimΚ³ pβ‚βŠ•pβ‚‚βˆ˜β–³ ⟩ + f βŠ•β‚ g ∎ + + β‰ˆΞ±β‡’ : {A B C : Obj} β†’ Ξ±β‡’β€² {A} {B} {C} β‰ˆ Ξ±β‡’ {A} {B} {C} + β‰ˆΞ±β‡’ {A} {B} {C} = begin + (p₁ ∘ p₁) βŠ•β‚ ((pβ‚‚ ∘ p₁) βŠ•β‚ pβ‚‚ ∘ β–³) ∘ β–³ β‰ˆβŸ¨ reflβŸ©βŠ—βŸ¨ pushΛ‘ split₁ˑ ⟩∘⟨refl ⟩ + (p₁ ∘ p₁) βŠ•β‚ ((pβ‚‚ βŠ•β‚ id) ∘ (p₁ βŠ•β‚ pβ‚‚) ∘ β–³) ∘ β–³ β‰ˆβŸ¨ reflβŸ©βŠ—βŸ¨ elimΚ³ pβ‚βŠ•pβ‚‚βˆ˜β–³ ⟩∘⟨refl ⟩ + (p₁ ∘ p₁) βŠ•β‚ (pβ‚‚ βŠ•β‚ id) ∘ β–³ β‰ˆβŸ¨ †-homomorphism βŸ©βŠ—βŸ¨ (reflβŸ©βŠ—βŸ¨ †-identity ) ⟩∘⟨refl ⟨ + ((i₁ ∘ i₁) †) βŠ•β‚ (pβ‚‚ βŠ•β‚ (id †)) ∘ β–³ β‰ˆβŸ¨ reflβŸ©βŠ—βŸ¨ †-resp-βŠ— ⟩∘⟨refl ⟨ + ((i₁ ∘ i₁) †) βŠ•β‚ ((iβ‚‚ βŠ•β‚ id) †) ∘ β–³ β‰ˆβŸ¨ †-resp-βŠ— ⟩∘⟨refl ⟨ + ((i₁ ∘ i₁) βŠ•β‚ (iβ‚‚ βŠ•β‚ id)) † ∘ β–³ β‰ˆβŸ¨ †-homomorphism ⟨ + (β–½ ∘ ((i₁ ∘ i₁) βŠ•β‚ (iβ‚‚ βŠ•β‚ id))) † β‰ˆβŸ¨ ⟨ β–½βˆ˜+₁ βŸ©β€  ⟩ + [ i₁ ∘ i₁ , iβ‚‚ βŠ•β‚ id ] † β‰ˆβŸ¨ ⟨ []-congΛ‘ ([]-congΛ‘ identityΚ³) βŸ©β€  ⟩ + α⇐ † β‰ˆβŸ¨ ⟨ α≅† βŸ©β€  ⟨ + Ξ±β‡’ † † β‰ˆβŸ¨ †-involutive Ξ±β‡’ ⟩ + Ξ±β‡’ ∎ + record IdempotentSemiadditiveDagger : Set (suc (o βŠ” β„“ βŠ” e)) where field diff --git a/Data/System.agda b/Data/System.agda index 968332d..7b6fe06 100644 --- a/Data/System.agda +++ b/Data/System.agda @@ -2,9 +2,9 @@ open import Level using (Level) -module Data.System {β„“ : Level} where +module Data.System {c β„“ : Level} where -open import Data.System.Core {β„“} public -open import Data.System.Category {β„“} public -open import Data.System.Looped {β„“} public -open import Data.System.Monoidal {β„“} public using (Systems-MC; Systems-SMC) +open import Data.System.Core {c} {β„“} public +open import Data.System.Category {c} {β„“} public +open import Data.System.Looped {c} {β„“} public +open import Data.System.Monoidal {c} {β„“} public using (Systems-MC; Systems-SMC) 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