diff options
Diffstat (limited to 'Data/WiringDiagram/Balanced.agda')
| -rw-r--r-- | Data/WiringDiagram/Balanced.agda | 65 |
1 files changed, 57 insertions, 8 deletions
diff --git a/Data/WiringDiagram/Balanced.agda b/Data/WiringDiagram/Balanced.agda index 09656fc..ada297b 100644 --- a/Data/WiringDiagram/Balanced.agda +++ b/Data/WiringDiagram/Balanced.agda @@ -10,29 +10,78 @@ module Data.WiringDiagram.Balanced (S : IdempotentSemiadditiveDagger 𝒞) where +import Categories.Category.Monoidal.Reasoning as ⊗-Reasoning +import Categories.Morphism.Reasoning as ⇒-Reasoning + open import Categories.Functor using (Functor) -open import Data.WiringDiagram.Core S using (WiringDiagram; _□_) +open import Data.WiringDiagram.Core S using (WiringDiagram; _□_; _⌸_; push) +open import Categories.Category.Monoidal.Utilities using (module Shorthands) +open import Categories.Category.Monoidal using (Monoidal) open import Data.WiringDiagram.Directed S using (DWD) -open import Function using (id) +open import Function using () renaming (id to idf) -open Category 𝒞 using (Obj) +module 𝒞 = Category 𝒞 +module DWD = Category DWD -- The category of balanced wiring diagrams BWD : Category o ℓ e BWD = record - { Obj = Obj + { Obj = 𝒞.Obj ; _⇒_ = λ A B → WiringDiagram (A □ A) (B □ B) - ; Category DWD + ; DWD } -- Inclusion functor from BWD to DWD Include : Functor BWD DWD Include = record { F₀ = λ A → A □ A - ; F₁ = id + ; F₁ = idf ; identity = Equiv.refl ; homomorphism = Equiv.refl - ; F-resp-≈ = id + ; F-resp-≈ = idf + } + where + open DWD using (module Equiv) + +-- Covariant functor from underlying category to BWD +Push : Functor 𝒞 BWD +Push = record + { F₀ = idf + ; F₁ = push + ; identity = elimˡ †-identity ⌸ Equiv.refl + ; homomorphism = λ {A B C f g} → homoᵢ f g ⌸ Equiv.refl + ; F-resp-≈ = λ f≈g → (†-resp-≈ f≈g ⟩∘⟨refl) ⌸ f≈g } where - open Category DWD using (module Equiv) + open Category 𝒞 + open IdempotentSemiadditiveDagger S + using (+-monoidal; _†; p₂; _⊕₁_; △; !; p₁; p₂-⊕; ⇒!; ⇒△; ρ⇒≈p₁; p₁∘△; †-homomorphism; †-identity; †-resp-≈) + open Monoidal +-monoidal using (assoc-commute-from; unitorˡ-commute-from; triangle) + open Shorthands +-monoidal using (α⇒; λ⇒; ρ⇒) + open ⇒-Reasoning 𝒞 + open ⊗-Reasoning +-monoidal + homoᵢ + : {A B C : Obj} + (f : A ⇒ B) + (g : B ⇒ C) + → (g ∘ f) † ∘ p₂ + ≈ (f † ∘ p₂) ∘ id ⊕₁ ((g † ∘ p₂) ∘ f ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id + homoᵢ f g = begin + (g ∘ f) † ∘ p₂ ≈⟨ pushˡ †-homomorphism ⟩ + f † ∘ g † ∘ p₂ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ p₂-⊕ ⟩ + f † ∘ g † ∘ λ⇒ ∘ ! ⊕₁ id ≈⟨ refl⟩∘⟨ extendʳ unitorˡ-commute-from ⟨ + f † ∘ λ⇒ ∘ id ⊕₁ (g †) ∘ ! ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ insertˡ p₁∘△ ⟩⊗⟨refl ⟩ + f † ∘ λ⇒ ∘ id ⊕₁ (g †) ∘ (p₁ ∘ △ ∘ !) ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ (ρ⇒≈p₁ ⟩∘⟨refl) ⟩⊗⟨refl ⟨ + f † ∘ λ⇒ ∘ id ⊕₁ (g †) ∘ (ρ⇒ ∘ △ ∘ !) ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ split₁ˡ ⟩ + f † ∘ λ⇒ ∘ id ⊕₁ (g †) ∘ ρ⇒ ⊕₁ id ∘ (△ ∘ !) ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ ⇒△ ⟩⊗⟨refl ⟩ + f † ∘ λ⇒ ∘ id ⊕₁ (g †) ∘ ρ⇒ ⊕₁ id ∘ (! ⊕₁ ! ∘ △) ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ split₁ˡ ⟩ + f † ∘ λ⇒ ∘ id ⊕₁ (g †) ∘ ρ⇒ ⊕₁ id ∘ (! ⊕₁ !) ⊕₁ id ∘ △ ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ (Equiv.sym triangle) ⟩ + f † ∘ λ⇒ ∘ id ⊕₁ (g †) ∘ id ⊕₁ λ⇒ ∘ α⇒ ∘ (! ⊕₁ !) ⊕₁ id ∘ △ ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ merge₂ˡ ⟩ + f † ∘ λ⇒ ∘ id ⊕₁ (g † ∘ λ⇒) ∘ α⇒ ∘ (! ⊕₁ !) ⊕₁ id ∘ △ ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ assoc-commute-from ⟩ + f † ∘ λ⇒ ∘ id ⊕₁ (g † ∘ λ⇒) ∘ ! ⊕₁ ! ⊕₁ id ∘ α⇒ ∘ △ ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ merge₂ˡ ⟩ + f † ∘ λ⇒ ∘ ! ⊕₁ ((g † ∘ λ⇒) ∘ ! ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩⊗⟨ (pullʳ (refl⟩∘⟨ (Equiv.sym ⇒! ⟩⊗⟨refl))) ⟩∘⟨refl ⟩ + f † ∘ λ⇒ ∘ ! ⊕₁ (g † ∘ λ⇒ ∘ (! ∘ f) ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩⊗⟨ (refl⟩∘⟨ (pushʳ split₁ˡ)) ⟩∘⟨refl ⟩ + f † ∘ λ⇒ ∘ ! ⊕₁ (g † ∘ (λ⇒ ∘ ! ⊕₁ id) ∘ f ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩⊗⟨ (pullˡ (refl⟩∘⟨ Equiv.sym p₂-⊕)) ⟩∘⟨refl ⟩ + f † ∘ λ⇒ ∘ ! ⊕₁ ((g † ∘ p₂) ∘ f ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id ≈⟨ pushʳ (extendʳ (pushʳ serialize₁₂)) ⟩ + (f † ∘ (λ⇒ ∘ ! ⊕₁ id)) ∘ id ⊕₁ ((g † ∘ p₂) ∘ f ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id ≈⟨ (refl⟩∘⟨ p₂-⊕) ⟩∘⟨refl ⟨ + (f † ∘ p₂) ∘ id ⊕₁ ((g † ∘ p₂) ∘ f ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id ∎ |