diff options
Diffstat (limited to 'Data')
| -rw-r--r-- | Data/WiringDiagram/Balanced.agda | 38 | ||||
| -rw-r--r-- | Data/WiringDiagram/Core.agda | 130 | ||||
| -rw-r--r-- | Data/WiringDiagram/Directed.agda | 184 | ||||
| -rw-r--r-- | Data/WiringDiagram/Full.agda | 261 |
4 files changed, 352 insertions, 261 deletions
diff --git a/Data/WiringDiagram/Balanced.agda b/Data/WiringDiagram/Balanced.agda new file mode 100644 index 0000000..09656fc --- /dev/null +++ b/Data/WiringDiagram/Balanced.agda @@ -0,0 +1,38 @@ +{-# OPTIONS --without-K --safe #-} + +open import Categories.Category using (Category) +open import Category.Dagger.Semiadditive using (IdempotentSemiadditiveDagger) +open import Level using (Level) + +module Data.WiringDiagram.Balanced + {o ℓ e : Level} + {𝒞 : Category o ℓ e} + (S : IdempotentSemiadditiveDagger 𝒞) + where + +open import Categories.Functor using (Functor) +open import Data.WiringDiagram.Core S using (WiringDiagram; _□_) +open import Data.WiringDiagram.Directed S using (DWD) +open import Function using (id) + +open Category 𝒞 using (Obj) + +-- The category of balanced wiring diagrams +BWD : Category o ℓ e +BWD = record + { Obj = Obj + ; _⇒_ = λ A B → WiringDiagram (A □ A) (B □ B) + ; Category DWD + } + +-- Inclusion functor from BWD to DWD +Include : Functor BWD DWD +Include = record + { F₀ = λ A → A □ A + ; F₁ = id + ; identity = Equiv.refl + ; homomorphism = Equiv.refl + ; F-resp-≈ = id + } + where + open Category DWD using (module Equiv) diff --git a/Data/WiringDiagram/Core.agda b/Data/WiringDiagram/Core.agda new file mode 100644 index 0000000..d2e01cd --- /dev/null +++ b/Data/WiringDiagram/Core.agda @@ -0,0 +1,130 @@ +{-# OPTIONS --without-K --safe #-} + +open import Categories.Category using (Category) +open import Level using (Level) +open import Category.Dagger.Semiadditive using (IdempotentSemiadditiveDagger) + +module Data.WiringDiagram.Core + {o ℓ e : Level} + {𝒞 : Category o ℓ e} + (S : IdempotentSemiadditiveDagger 𝒞) + where + +open import Categories.Category.Monoidal.Utilities using (module Shorthands) +open import Relation.Binary using (IsEquivalence) + +open Category 𝒞 using (Obj; _∘_; _⇒_; id; _≈_; module Equiv) +open IdempotentSemiadditiveDagger S using (_⊕₀_; _⊕₁_; p₂; +-monoidal; △; ▽) +open Shorthands +-monoidal using (α⇒) + +-- A "Box" is a pair of objects from the underlying category, +-- representing input and output ports +-- +-----------+ +-- | | +-- Aᵢ A Aₒ +-- | | +-- +-----------+ +record Box : Set o where + + constructor _□_ + + field + ᵢ : Obj + ₒ : Obj + +infix 4 _□_ + +-- A Wiring Diagram between two boxes +-- is a pair of morphisms from the underlying category +-- (which can be thought of as generalized relations): +-- 1. A relation from the output of the inner box +-- plus the input of the outer box to the input of +-- the inner box +-- 2. A relation from the output of the inner box +-- to the output of the outer box +-- This choice of definition gives a way to represent +-- feedback from output to input. +-- +-- outer box (B) +-- +--------------------------------+ +-- | | +-- | /-------------------\ | +-- | | | | +-- | | +-------+ | | +-- | \----| | | | +-- | Aₒ ⊕ Bᵢ | inner |------+------| +-- | ⇒ Aᵢ | box | Aₒ ⇒ Bₒ | +-- |----------| (A) | output | +-- | input | | relation | +-- | relation +-------+ | +-- | | +-- +--------------------------------+ +record WiringDiagram (A B : Box) : Set ℓ where + + constructor _⧈_ + + private + module A = Box A + module B = Box B + + field + input : A.ₒ ⊕₀ B.ᵢ ⇒ A.ᵢ + output : A.ₒ ⇒ B.ₒ + +infix 4 _⧈_ + +-- Two wiring diagrams are equivalent when their +-- input and output relations are equivalent as +-- morphism in the underlying category. +record _≈-⧈_ {A B : Box} (f g : WiringDiagram A B) : Set e where + + constructor _⌸_ + + private + + module f = WiringDiagram f + module g = WiringDiagram g + + field + ≈i : f.input ≈ g.input + ≈o : f.output ≈ g.output + +infix 4 _≈-⧈_ + +-- Equivalence of boxes is a legitimate equivalence relation +module _ {A B : Box} where + + open Equiv + + ≈-refl : {x : WiringDiagram A B} → x ≈-⧈ x + ≈-refl = refl ⌸ refl + + ≈-sym : {x y : WiringDiagram A B} → x ≈-⧈ y → y ≈-⧈ x + ≈-sym (≈i ⌸ ≈o) = sym ≈i ⌸ sym ≈o + + ≈-trans : {x y z : WiringDiagram A B} → x ≈-⧈ y → y ≈-⧈ z → x ≈-⧈ z + ≈-trans (≈i₁ ⌸ ≈o₁) (≈i₂ ⌸ ≈o₂) = trans ≈i₁ ≈i₂ ⌸ trans ≈o₁ ≈o₂ + + ≈-isEquiv : IsEquivalence (_≈-⧈_ {A} {B}) + ≈-isEquiv = record + { refl = ≈-refl + ; sym = ≈-sym + ; trans = ≈-trans + } + +-- The identity wiring diagram +id-⧈ : {A : Box} → WiringDiagram A A +id-⧈ = p₂ ⧈ id + +-- Composition of wiring diagrams +_⌻_ : {A B C : Box} → WiringDiagram B C → WiringDiagram A B → WiringDiagram A C +_⌻_ {Aᵢ □ Aₒ} {Bᵢ □ Bₒ} {Cᵢ □ Cₒ} (f′ ⧈ g′) (f ⧈ g) = f″ ⧈ g′ ∘ g + where + f″ : Aₒ ⊕₀ Cᵢ ⇒ Aᵢ + f″ = f ∘ id ⊕₁ (f′ ∘ g ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id + +infixr 9 _⌻_ + +-- The loop wiring diagram +loop : {A : Obj} → WiringDiagram (A □ A) (A □ A) +loop = ▽ ⧈ id diff --git a/Data/WiringDiagram/Directed.agda b/Data/WiringDiagram/Directed.agda new file mode 100644 index 0000000..88c6008 --- /dev/null +++ b/Data/WiringDiagram/Directed.agda @@ -0,0 +1,184 @@ +{-# OPTIONS --without-K --safe #-} + +open import Categories.Category using (Category) +open import Category.Dagger.Semiadditive using (IdempotentSemiadditiveDagger) +open import Level using (Level) + +module Data.WiringDiagram.Directed + {o ℓ e : Level} + {𝒞 : Category o ℓ e} + (S : IdempotentSemiadditiveDagger 𝒞) + where + +import Categories.Category.Monoidal.Properties as ⊗-Properties +import Categories.Category.Monoidal.Reasoning as ⊗-Reasoning +import Categories.Morphism.Reasoning as ⇒-Reasoning + +open import Categories.Category.Helper using (categoryHelper) +open import Categories.Category.Monoidal using (Monoidal) +open import Categories.Category.Monoidal.Utilities using (module Shorthands) +open import Data.WiringDiagram.Core S using (Box; WiringDiagram; _≈-⧈_; _□_; _⧈_; _⌸_; id-⧈; _⌻_; ≈-isEquiv) + +open Category 𝒞 +open IdempotentSemiadditiveDagger S +open Monoidal +-monoidal +open Shorthands +-monoidal using (α⇒; α⇐; λ⇒; λ⇐; ρ⇒; ρ⇐) +open ⊗-Properties +-monoidal using (coherence₁) + +private + + ⌻-resp-≈ : {A B C : Box} {f h : WiringDiagram B C} {g i : WiringDiagram A B} → f ≈-⧈ h → g ≈-⧈ i → f ⌻ g ≈-⧈ h ⌻ i + ⌻-resp-≈ {A} {B} {C} {fᵢ ⧈ fₒ} {hᵢ ⧈ hₒ} {gᵢ ⧈ gₒ} {iᵢ ⧈ iₒ} (fᵢ≈hᵢ ⌸ fₒ≈hₒ) (gᵢ≈iᵢ ⌸ gₒ≈iₒ) = ≈ᵢ ⌸ ∘-resp-≈ fₒ≈hₒ gₒ≈iₒ + where + open ⊗-Reasoning +-monoidal + ≈ᵢ : gᵢ ∘ id ⊕₁ (fᵢ ∘ gₒ ⊕₁ id) ∘ α⇒ ∘ △ {Box.ₒ A} ⊕₁ id + ≈ iᵢ ∘ id ⊕₁ (hᵢ ∘ iₒ ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id + ≈ᵢ = gᵢ≈iᵢ ⟩∘⟨ refl⟩⊗⟨ (fᵢ≈hᵢ ⟩∘⟨ gₒ≈iₒ ⟩⊗⟨refl) ⟩∘⟨refl + + ⌻-assoc : {A B C D : Box} {f : WiringDiagram A B} {g : WiringDiagram B C} {h : WiringDiagram C D} → (h ⌻ g) ⌻ f ≈-⧈ h ⌻ (g ⌻ f) + ⌻-assoc {Aᵢ □ Aₒ} {Bᵢ □ Bₒ} {Cᵢ □ Cₒ} {Dᵢ □ Dₒ} {fᵢ ⧈ fₒ} {gᵢ ⧈ gₒ} {hᵢ ⧈ hₒ} = ≈ᵢ ⌸ assoc + where + open ⊗-Reasoning +-monoidal + + term₁ : Aₒ ⊕₀ Dᵢ ⇒ Cᵢ + term₁ = hᵢ ∘ (gₒ ∘ fₒ) ⊕₁ id + + term₂ : Bₒ ⊕₀ Dᵢ ⇒ Cᵢ + term₂ = hᵢ ∘ gₒ ⊕₁ id + + term₃ : Aₒ ⊕₀ Cᵢ ⇒ Bᵢ + term₃ = gᵢ ∘ fₒ ⊕₁ id + open ⇒-Reasoning 𝒞 + + lemma₁ : α⇒ {Aₒ ⊕₀ Aₒ} {Aₒ} {Dᵢ} ∘ (α⇐ ∘ id ⊕₁ △) ⊕₁ id ∘ △ ⊕₁ id ≈ △ ⊕₁ id ∘ α⇒ ∘ △ ⊕₁ id + lemma₁ = begin + α⇒ ∘ (α⇐ ∘ id ⊕₁ △) ⊕₁ id ∘ △ ⊕₁ id ≈⟨ refl⟩∘⟨ pushˡ split₁ˡ ⟩ + α⇒ ∘ α⇐ ⊕₁ id ∘ (id ⊕₁ △) ⊕₁ id ∘ △ ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ merge₁ˡ ⟩ + α⇒ ∘ α⇐ ⊕₁ id ∘ (id ⊕₁ △ ∘ △) ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ △-assoc ⟩⊗⟨refl ⟩ + α⇒ ∘ α⇐ ⊕₁ id ∘ (α⇒ ∘ △ ⊕₁ id ∘ △) ⊕₁ id ≈⟨ refl⟩∘⟨ merge₁ʳ ⟩ + α⇒ ∘ (α⇐ ∘ α⇒ ∘ △ ⊕₁ id ∘ △) ⊕₁ id ≈⟨ refl⟩∘⟨ cancelˡ associator.isoˡ ⟩⊗⟨refl ⟩ + α⇒ ∘ (△ ⊕₁ id ∘ △) ⊕₁ id ≈⟨ refl⟩∘⟨ split₁ˡ ⟩ + α⇒ ∘ (△ ⊕₁ id) ⊕₁ id ∘ △ ⊕₁ id ≈⟨ extendʳ assoc-commute-from ⟩ + △ ⊕₁ id ⊕₁ id ∘ α⇒ ∘ △ ⊕₁ id ≈⟨ refl⟩⊗⟨ ⊕.identity ⟩∘⟨refl ⟩ + △ ⊕₁ id ∘ α⇒ ∘ △ ⊕₁ id ∎ + + lemma₂ : △ ⊕₁ id {Dᵢ} ∘ fₒ ⊕₁ id ≈ (fₒ ⊕₁ fₒ) ⊕₁ id ∘ △ ⊕₁ id + lemma₂ = begin + △ ⊕₁ id ∘ fₒ ⊕₁ id ≈⟨ merge₁ʳ ⟩ + (△ ∘ fₒ) ⊕₁ id ≈⟨ ⇒△ ⟩⊗⟨refl ⟩ + (fₒ ⊕₁ fₒ ∘ △) ⊕₁ id ≈⟨ split₁ʳ ⟩ + (fₒ ⊕₁ fₒ) ⊕₁ id ∘ △ ⊕₁ id ∎ + + ≈ᵢ : fᵢ ∘ id ⊕₁ ((gᵢ ∘ id ⊕₁ (hᵢ ∘ gₒ ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id) ∘ fₒ ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id + ≈ (fᵢ ∘ id ⊕₁ (gᵢ ∘ fₒ ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id) ∘ id ⊕₁ (hᵢ ∘ (gₒ ∘ fₒ) ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id + ≈ᵢ = begin + fᵢ ∘ id ⊕₁ ((gᵢ ∘ id ⊕₁ term₂ ∘ α⇒ ∘ △ ⊕₁ id) ∘ fₒ ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id + ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ extendˡ (extendˡ assoc) ⟩∘⟨refl ⟩ + fᵢ ∘ id ⊕₁ ((gᵢ ∘ id ⊕₁ term₂ ∘ α⇒) ∘ △ ⊕₁ id ∘ fₒ ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id + ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ (refl⟩∘⟨ lemma₂) ⟩∘⟨refl ⟩ + fᵢ ∘ id ⊕₁ ((gᵢ ∘ id ⊕₁ term₂ ∘ α⇒) ∘ (fₒ ⊕₁ fₒ) ⊕₁ id ∘ △ ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id + ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ extendˡ assoc ⟩∘⟨refl ⟩ + fᵢ ∘ id ⊕₁ ((gᵢ ∘ id ⊕₁ term₂) ∘ α⇒ ∘ (fₒ ⊕₁ fₒ) ⊕₁ id ∘ △ ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id + ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ (refl⟩∘⟨ extendʳ assoc-commute-from ) ⟩∘⟨refl ⟩ + fᵢ ∘ id ⊕₁ ((gᵢ ∘ id ⊕₁ term₂) ∘ fₒ ⊕₁ fₒ ⊕₁ id ∘ α⇒ ∘ △ ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id + ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ assoc ⟩∘⟨refl ⟩ + fᵢ ∘ id ⊕₁ (gᵢ ∘ id ⊕₁ term₂ ∘ fₒ ⊕₁ fₒ ⊕₁ id ∘ α⇒ ∘ △ ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id + ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ (refl⟩∘⟨ pullˡ merge₂ˡ ) ⟩∘⟨refl ⟩ + fᵢ ∘ id ⊕₁ (gᵢ ∘ fₒ ⊕₁ (term₂ ∘ fₒ ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id + ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ (refl⟩∘⟨ refl⟩⊗⟨ pullʳ merge₁ʳ ⟩∘⟨refl) ⟩∘⟨refl ⟩ + fᵢ ∘ id ⊕₁ (gᵢ ∘ fₒ ⊕₁ term₁ ∘ α⇒ ∘ △ ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id + ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ assoc ⟩∘⟨refl ⟨ + fᵢ ∘ id ⊕₁ ((gᵢ ∘ fₒ ⊕₁ term₁) ∘ α⇒ ∘ △ ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id + ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ extendˡ assoc ⟩∘⟨refl ⟨ + fᵢ ∘ id ⊕₁ ((gᵢ ∘ fₒ ⊕₁ term₁ ∘ α⇒) ∘ △ ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id + ≈⟨ refl⟩∘⟨ pushˡ split₂ʳ ⟩ + fᵢ ∘ id ⊕₁ (gᵢ ∘ fₒ ⊕₁ term₁ ∘ α⇒) ∘ id ⊕₁ △ ⊕₁ id ∘ α⇒ ∘ △ ⊕₁ id + ≈⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ assoc-commute-from ⟨ + fᵢ ∘ id ⊕₁ (gᵢ ∘ fₒ ⊕₁ term₁ ∘ α⇒) ∘ α⇒ ∘ (id ⊕₁ △) ⊕₁ id ∘ △ ⊕₁ id + ≈⟨ refl⟩∘⟨ extendʳ (refl⟩⊗⟨ assoc ⟩∘⟨refl) ⟨ + fᵢ ∘ id ⊕₁ ((gᵢ ∘ fₒ ⊕₁ term₁) ∘ α⇒) ∘ α⇒ ∘ (id ⊕₁ △) ⊕₁ id ∘ △ ⊕₁ id + ≈⟨ refl⟩∘⟨ pushˡ split₂ʳ ⟩ + fᵢ ∘ id ⊕₁ (gᵢ ∘ fₒ ⊕₁ term₁) ∘ id ⊕₁ α⇒ ∘ α⇒ ∘ (id ⊕₁ △) ⊕₁ id ∘ △ ⊕₁ id + ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ insertˡ associator.isoʳ ⟩⊗⟨refl ⟩∘⟨refl ⟩ + fᵢ ∘ id ⊕₁ (gᵢ ∘ fₒ ⊕₁ term₁) ∘ id ⊕₁ α⇒ ∘ α⇒ ∘ (α⇒ ∘ α⇐ ∘ id ⊕₁ △) ⊕₁ id ∘ △ ⊕₁ id + ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ split₁ʳ ⟩ + fᵢ ∘ id ⊕₁ (gᵢ ∘ fₒ ⊕₁ term₁) ∘ id ⊕₁ α⇒ ∘ α⇒ ∘ α⇒ ⊕₁ id ∘ (α⇐ ∘ id ⊕₁ △) ⊕₁ id ∘ △ ⊕₁ id + ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ assoc ⟨ + fᵢ ∘ id ⊕₁ (gᵢ ∘ fₒ ⊕₁ term₁) ∘ id ⊕₁ α⇒ ∘ (α⇒ ∘ α⇒ ⊕₁ id) ∘ (α⇐ ∘ id ⊕₁ △) ⊕₁ id ∘ △ ⊕₁ id + ≈⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ pentagon ⟩ + fᵢ ∘ id ⊕₁ (gᵢ ∘ fₒ ⊕₁ term₁) ∘ α⇒ ∘ α⇒ ∘ (α⇐ ∘ id ⊕₁ △) ⊕₁ id ∘ △ ⊕₁ id + ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ pushʳ serialize₁₂ ⟩∘⟨refl ⟩ + fᵢ ∘ id ⊕₁ (term₃ ∘ id ⊕₁ term₁) ∘ α⇒ ∘ α⇒ ∘ (α⇐ ∘ id ⊕₁ △) ⊕₁ id ∘ △ ⊕₁ id + ≈⟨ refl⟩∘⟨ pushˡ split₂ʳ ⟩ + fᵢ ∘ id ⊕₁ term₃ ∘ id ⊕₁ id ⊕₁ term₁ ∘ α⇒ ∘ α⇒ ∘ (α⇐ ∘ id ⊕₁ △) ⊕₁ id ∘ △ ⊕₁ id + ≈⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ assoc-commute-from ⟨ + fᵢ ∘ id ⊕₁ term₃ ∘ α⇒ ∘ (id ⊕₁ id) ⊕₁ term₁ ∘ α⇒ ∘ (α⇐ ∘ id ⊕₁ △) ⊕₁ id ∘ △ ⊕₁ id + ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ ⊕.identity ⟩⊗⟨refl ⟩∘⟨refl ⟩ + fᵢ ∘ id ⊕₁ term₃ ∘ α⇒ ∘ id ⊕₁ term₁ ∘ α⇒ ∘ (α⇐ ∘ id ⊕₁ △) ⊕₁ id ∘ △ ⊕₁ id + ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ lemma₁ ⟩ + fᵢ ∘ id ⊕₁ term₃ ∘ α⇒ ∘ id ⊕₁ term₁ ∘ △ ⊕₁ id ∘ α⇒ ∘ △ ⊕₁ id + ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ (Equiv.sym serialize₂₁ ○ serialize₁₂) ⟩ + fᵢ ∘ id ⊕₁ term₃ ∘ α⇒ ∘ △ ⊕₁ id ∘ id ⊕₁ term₁ ∘ α⇒ ∘ △ ⊕₁ id + ≈⟨ refl⟩∘⟨ refl⟩∘⟨ assoc ⟨ + fᵢ ∘ id ⊕₁ term₃ ∘ (α⇒ ∘ △ ⊕₁ id) ∘ id ⊕₁ term₁ ∘ α⇒ ∘ △ ⊕₁ id + ≈⟨ refl⟩∘⟨ assoc ⟨ + fᵢ ∘ (id ⊕₁ term₃ ∘ α⇒ ∘ △ ⊕₁ id) ∘ id ⊕₁ term₁ ∘ α⇒ ∘ △ ⊕₁ id + ≈⟨ assoc ⟨ + (fᵢ ∘ id ⊕₁ term₃ ∘ α⇒ ∘ △ ⊕₁ id) ∘ id ⊕₁ term₁ ∘ α⇒ ∘ △ ⊕₁ id ∎ + + ⌻-identityˡ : {A B : Box} {f : WiringDiagram A B} → id-⧈ ⌻ f ≈-⧈ f + ⌻-identityˡ {Aᵢ □ Aₒ} {Bᵢ □ Bₒ} {fᵢ ⧈ fₒ} = ≈ᵢ ⌸ identityˡ + where + open ⇒-Reasoning 𝒞 + open ⊗-Reasoning +-monoidal + ≈ᵢ : fᵢ ∘ id ⊕₁ (p₂ ∘ fₒ ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id ≈ fᵢ + ≈ᵢ = begin + fᵢ ∘ id ⊕₁ (p₂ ∘ fₒ ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ (p₂-⊕ ⟩∘⟨refl) ⟩∘⟨refl ⟩ + fᵢ ∘ id ⊕₁ ((λ⇒ ∘ ! ⊕₁ id) ∘ fₒ ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ pullʳ merge₁ʳ ⟩∘⟨refl ⟩ + fᵢ ∘ id ⊕₁ (λ⇒ ∘ (! ∘ fₒ) ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ (refl⟩∘⟨ ⇒! ⟩⊗⟨refl) ⟩∘⟨refl ⟩ + fᵢ ∘ id ⊕₁ (λ⇒ ∘ ! ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id ≈⟨ refl⟩∘⟨ pushˡ split₂ʳ ⟩ + fᵢ ∘ id ⊕₁ λ⇒ ∘ id ⊕₁ ! ⊕₁ id ∘ α⇒ ∘ △ ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ assoc-commute-from ⟨ + fᵢ ∘ id ⊕₁ λ⇒ ∘ α⇒ ∘ (id ⊕₁ !) ⊕₁ id ∘ △ ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ merge₁ˡ ⟩ + fᵢ ∘ id ⊕₁ λ⇒ ∘ α⇒ ∘ (id ⊕₁ ! ∘ △) ⊕₁ id ≈⟨ refl⟩∘⟨ pullˡ triangle ⟩ + fᵢ ∘ ρ⇒ ⊕₁ id ∘ (id ⊕₁ ! ∘ △) ⊕₁ id ≈⟨ refl⟩∘⟨ merge₁ʳ ⟩ + fᵢ ∘ (ρ⇒ ∘ id ⊕₁ ! ∘ △) ⊕₁ id ≈⟨ refl⟩∘⟨ (refl⟩∘⟨ △-identityʳ ) ⟩⊗⟨refl ⟩ + fᵢ ∘ (ρ⇒ ∘ ρ⇐) ⊕₁ id ≈⟨ refl⟩∘⟨ unitorʳ.isoʳ ⟩⊗⟨refl ⟩ + fᵢ ∘ id ⊕₁ id ≈⟨ elimʳ ⊕.identity ⟩ + fᵢ ∎ + + ⌻-identityʳ : {A B : Box} {f : WiringDiagram A B} → f ⌻ id-⧈ ≈-⧈ f + ⌻-identityʳ {Aᵢ □ Aₒ} {Bᵢ □ Bₒ} {fᵢ ⧈ fₒ} = ≈ᵢ ⌸ identityʳ + where + open ⇒-Reasoning 𝒞 + open ⊗-Reasoning +-monoidal + ≈ᵢ : p₂ ∘ id ⊕₁ (fᵢ ∘ id ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id ≈ fᵢ + ≈ᵢ = begin + p₂ ∘ id ⊕₁ (fᵢ ∘ id ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id ≈⟨ p₂-⊕ ⟩∘⟨refl ⟩ + (λ⇒ ∘ ! ⊕₁ id) ∘ id ⊕₁ (fᵢ ∘ id ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ elimʳ ⊕.identity ⟩∘⟨refl ⟩ + (λ⇒ ∘ ! ⊕₁ id) ∘ id ⊕₁ fᵢ ∘ α⇒ ∘ △ ⊕₁ id ≈⟨ pullˡ (pullʳ (Equiv.sym serialize₁₂)) ⟩ + (λ⇒ ∘ ! ⊕₁ fᵢ) ∘ α⇒ ∘ △ ⊕₁ id ≈⟨ pullʳ (pushˡ serialize₂₁) ⟩ + λ⇒ ∘ id ⊕₁ fᵢ ∘ ! ⊕₁ id ∘ α⇒ ∘ △ ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩⊗⟨ ⊕.identity ⟩∘⟨refl ⟨ + λ⇒ ∘ id ⊕₁ fᵢ ∘ ! ⊕₁ id ⊕₁ id ∘ α⇒ ∘ △ ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ assoc-commute-from ⟨ + λ⇒ ∘ id ⊕₁ fᵢ ∘ α⇒ ∘ (! ⊕₁ id) ⊕₁ id ∘ △ ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ merge₁ʳ ⟩ + λ⇒ ∘ id ⊕₁ fᵢ ∘ α⇒ ∘ (! ⊕₁ id ∘ △) ⊕₁ id ≈⟨ extendʳ unitorˡ-commute-from ⟩ + fᵢ ∘ λ⇒ ∘ α⇒ ∘ (! ⊕₁ id ∘ △) ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ △-identityˡ ⟩⊗⟨refl ⟩ + fᵢ ∘ λ⇒ ∘ α⇒ ∘ λ⇐ ⊕₁ id ≈⟨ refl⟩∘⟨ pullˡ coherence₁ ⟩ + fᵢ ∘ λ⇒ ⊕₁ id ∘ λ⇐ ⊕₁ id ≈⟨ refl⟩∘⟨ merge₁ʳ ⟩ + fᵢ ∘ (λ⇒ ∘ λ⇐) ⊕₁ id ≈⟨ refl⟩∘⟨ unitorˡ.isoʳ ⟩⊗⟨refl ⟩ + fᵢ ∘ id ⊕₁ id ≈⟨ elimʳ ⊕.identity ⟩ + fᵢ ∎ + +-- The category of directed wiring diagrams +DWD : Category o ℓ e +DWD = categoryHelper record + { Obj = Box + ; _⇒_ = WiringDiagram + ; _≈_ = _≈-⧈_ + ; id = id-⧈ + ; _∘_ = _⌻_ + ; assoc = ⌻-assoc + ; identityˡ = ⌻-identityˡ + ; identityʳ = ⌻-identityʳ + ; equiv = ≈-isEquiv + ; ∘-resp-≈ = ⌻-resp-≈ + } diff --git a/Data/WiringDiagram/Full.agda b/Data/WiringDiagram/Full.agda deleted file mode 100644 index 8cfe9eb..0000000 --- a/Data/WiringDiagram/Full.agda +++ /dev/null @@ -1,261 +0,0 @@ -{-# OPTIONS --without-K --safe #-} - -open import Categories.Category using (Category) -open import Categories.Category.Monoidal using (Monoidal) -open import Level using (Level) - -module Data.WiringDiagram.Full {o ℓ e : Level} {𝒞 : Category o ℓ e} (M : Monoidal 𝒞) where - -open import Categories.Category.Helper using (categoryHelper) -open import Relation.Binary using (IsEquivalence) - -module U = Category 𝒞 -module M = Monoidal M -open M - -record Box : Set o where - - constructor _□_ - - field - ᵢ : U.Obj - ₒ : U.Obj - -infix 4 _□_ - -record WiringDiagram (A B : Box) : Set ℓ where - - constructor _⧈_ - - private - module A = Box A - module B = Box B - - field - input : A.ₒ ⊗₀ B.ᵢ U.⇒ A.ᵢ - output : A.ₒ U.⇒ B.ₒ - -infix 4 _⧈_ - -record _≈_ {A B : Box} (f g : WiringDiagram A B) : Set e where - - constructor _⌸_ - - private - - module f = WiringDiagram f - module g = WiringDiagram g - - field - ≈i : f.input U.≈ g.input - ≈o : f.output U.≈ g.output - -infix 4 _≈_ - -module _ {A B : Box} where - - ≈-refl : {x : WiringDiagram A B} → x ≈ x - ≈-refl = U.Equiv.refl ⌸ U.Equiv.refl - - ≈-sym : {x y : WiringDiagram A B} → x ≈ y → y ≈ x - ≈-sym (≈i ⌸ ≈o) = U.Equiv.sym ≈i ⌸ U.Equiv.sym ≈o - - ≈-trans : {x y z : WiringDiagram A B} → x ≈ y → y ≈ z → x ≈ z - ≈-trans (≈i₁ ⌸ ≈o₁) (≈i₂ ⌸ ≈o₂) = U.Equiv.trans ≈i₁ ≈i₂ ⌸ U.Equiv.trans ≈o₁ ≈o₂ - - ≈-isEquiv : IsEquivalence (_≈_ {A} {B}) - ≈-isEquiv = record - { refl = ≈-refl - ; sym = ≈-sym - ; trans = ≈-trans - } - -open import Categories.Object.Monoid using (IsMonoid) -open import Categories.Category.Monoidal.Properties M using (coherence₁) renaming (monoidal-Op to Mᵒᵖ) - -comonoid : {A : U.Obj} → IsMonoid Mᵒᵖ A -comonoid = ? - -discard : {A : U.Obj} → A U.⇒ unit -discard = IsMonoid.η comonoid - -copy : {A : U.Obj} → A U.⇒ A ⊗₀ A -copy = IsMonoid.μ comonoid - -module _ {A B : U.Obj} {f : A U.⇒ B} where - - μ⇒ : copy U.∘ f U.≈ f ⊗₁ f U.∘ copy - μ⇒ = ? - - η⇒ : discard U.∘ f U.≈ discard - η⇒ = ? - -⊗-snd : {A B : U.Obj} → A ⊗₀ B U.⇒ B -⊗-snd {A} {B} = unitorˡ.from U.∘ discard ⊗₁ U.id - -id : {A : Box} → WiringDiagram A A -id {A} = ⊗-snd ⧈ U.id - -_∘_ : {A B C : Box} → WiringDiagram B C → WiringDiagram A B → WiringDiagram A C -_∘_ {Aᵢ □ Aₒ} {Bᵢ □ Bₒ} {Cᵢ □ Cₒ} (f′ ⧈ g′) (f ⧈ g) = f″ ⧈ g′ U.∘ g - where - f″ : Aₒ ⊗₀ Cᵢ U.⇒ Aᵢ - f″ = f U.∘ U.id ⊗₁ (f′ U.∘ g ⊗₁ U.id) U.∘ associator.from U.∘ copy ⊗₁ U.id - -import Categories.Category.Monoidal.Reasoning as ⊗-Reasoning -open import Categories.Category.Monoidal.Utilities M using (module Shorthands) -open Shorthands using (α⇒; α⇐; λ⇒; λ⇐; ρ⇒; ρ⇐) -import Categories.Morphism.Reasoning as ⇒-Reasoning - -∘-resp-≈ : {A B C : Box} {f h : WiringDiagram B C} {g i : WiringDiagram A B} → f ≈ h → g ≈ i → f ∘ g ≈ h ∘ i -∘-resp-≈ {A} {B} {C} {fᵢ ⧈ fₒ} {hᵢ ⧈ hₒ} {gᵢ ⧈ gₒ} {iᵢ ⧈ iₒ} (fᵢ≈hᵢ ⌸ fₒ≈hₒ) (gᵢ≈iᵢ ⌸ gₒ≈iₒ) = ≈ᵢ ⌸ U.∘-resp-≈ fₒ≈hₒ gₒ≈iₒ - where - open ⊗-Reasoning M - ≈ᵢ : gᵢ U.∘ U.id ⊗₁ (fᵢ U.∘ gₒ ⊗₁ U.id) U.∘ α⇒ U.∘ copy {Box.ₒ A} ⊗₁ U.id - U.≈ iᵢ U.∘ U.id ⊗₁ (hᵢ U.∘ iₒ ⊗₁ U.id) U.∘ α⇒ U.∘ copy ⊗₁ U.id - ≈ᵢ = gᵢ≈iᵢ ⟩∘⟨ refl⟩⊗⟨ (fᵢ≈hᵢ ⟩∘⟨ gₒ≈iₒ ⟩⊗⟨refl) ⟩∘⟨refl - -assoc : {A B C D : Box} {f : WiringDiagram A B} {g : WiringDiagram B C} {h : WiringDiagram C D} → (h ∘ g) ∘ f ≈ h ∘ (g ∘ f) -assoc {Aᵢ □ Aₒ} {Bᵢ □ Bₒ} {Cᵢ □ Cₒ} {Dᵢ □ Dₒ} {fᵢ ⧈ fₒ} {gᵢ ⧈ gₒ} {hᵢ ⧈ hₒ} = ≈ᵢ ⌸ U.assoc - where - open ⊗-Reasoning M - - term₁ : Aₒ ⊗₀ Dᵢ U.⇒ Cᵢ - term₁ = hᵢ U.∘ (gₒ U.∘ fₒ) ⊗₁ U.id - - term₂ : Bₒ ⊗₀ Dᵢ U.⇒ Cᵢ - term₂ = hᵢ U.∘ gₒ ⊗₁ U.id - - term₃ : Aₒ ⊗₀ Cᵢ U.⇒ Bᵢ - term₃ = gᵢ U.∘ fₒ ⊗₁ U.id - open ⇒-Reasoning 𝒞 - - lemma₁ : α⇒ {Aₒ ⊗₀ Aₒ} {Aₒ} {Dᵢ} U.∘ (α⇐ U.∘ U.id ⊗₁ copy) ⊗₁ U.id U.∘ copy ⊗₁ U.id U.≈ copy ⊗₁ U.id U.∘ α⇒ U.∘ copy ⊗₁ U.id - lemma₁ = begin - α⇒ U.∘ (α⇐ U.∘ U.id ⊗₁ copy) ⊗₁ U.id U.∘ copy ⊗₁ U.id ≈⟨ refl⟩∘⟨ pushˡ split₁ˡ ⟩ - α⇒ U.∘ α⇐ ⊗₁ U.id U.∘ (U.id ⊗₁ copy) ⊗₁ U.id U.∘ copy ⊗₁ U.id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ merge₁ˡ ⟩ - α⇒ U.∘ α⇐ ⊗₁ U.id U.∘ (U.id ⊗₁ copy U.∘ copy) ⊗₁ U.id ≈⟨ refl⟩∘⟨ merge₁ˡ ⟩ - α⇒ U.∘ (α⇐ U.∘ U.id ⊗₁ copy U.∘ copy) ⊗₁ U.id ≈⟨ refl⟩∘⟨ U.assoc ⟩⊗⟨refl ⟨ - α⇒ U.∘ ((α⇐ U.∘ U.id ⊗₁ copy) U.∘ copy) ⊗₁ U.id ≈⟨ refl⟩∘⟨ IsMonoid.assoc comonoid ⟩⊗⟨refl ⟨ - α⇒ U.∘ (copy ⊗₁ U.id U.∘ copy) ⊗₁ U.id ≈⟨ refl⟩∘⟨ split₁ˡ ⟩ - α⇒ U.∘ (copy ⊗₁ U.id) ⊗₁ U.id U.∘ copy ⊗₁ U.id ≈⟨ extendʳ assoc-commute-from ⟩ - copy ⊗₁ U.id ⊗₁ U.id U.∘ α⇒ U.∘ copy ⊗₁ U.id ≈⟨ refl⟩⊗⟨ ⊗.identity ⟩∘⟨refl ⟩ - copy ⊗₁ U.id U.∘ α⇒ U.∘ copy ⊗₁ U.id ∎ - - lemma₂ : copy ⊗₁ U.id U.∘ fₒ ⊗₁ U.id U.≈ (fₒ ⊗₁ fₒ) ⊗₁ U.id U.∘ copy ⊗₁ U.id - lemma₂ = begin - copy ⊗₁ U.id U.∘ fₒ ⊗₁ U.id ≈⟨ merge₁ʳ ⟩ - (copy U.∘ fₒ) ⊗₁ U.id ≈⟨ μ⇒ ⟩⊗⟨refl ⟩ - (fₒ ⊗₁ fₒ U.∘ copy) ⊗₁ U.id ≈⟨ split₁ʳ ⟩ - (fₒ ⊗₁ fₒ) ⊗₁ U.id U.∘ copy ⊗₁ U.id ∎ - - ≈ᵢ : fᵢ U.∘ U.id ⊗₁ ((gᵢ U.∘ U.id ⊗₁ (hᵢ U.∘ gₒ ⊗₁ U.id) U.∘ α⇒ U.∘ copy ⊗₁ U.id) U.∘ fₒ ⊗₁ U.id) U.∘ α⇒ U.∘ copy ⊗₁ U.id - U.≈ (fᵢ U.∘ U.id ⊗₁ (gᵢ U.∘ fₒ ⊗₁ U.id) U.∘ α⇒ U.∘ copy ⊗₁ U.id) U.∘ U.id ⊗₁ (hᵢ U.∘ (gₒ U.∘ fₒ) ⊗₁ U.id) U.∘ α⇒ U.∘ copy ⊗₁ U.id - ≈ᵢ = begin - fᵢ U.∘ U.id ⊗₁ ((gᵢ U.∘ U.id ⊗₁ term₂ U.∘ α⇒ U.∘ copy ⊗₁ U.id) U.∘ fₒ ⊗₁ U.id) U.∘ α⇒ U.∘ copy ⊗₁ U.id - ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ extendˡ (extendˡ U.assoc) ⟩∘⟨refl ⟩ - fᵢ U.∘ U.id ⊗₁ ((gᵢ U.∘ U.id ⊗₁ term₂ U.∘ α⇒) U.∘ copy ⊗₁ U.id U.∘ fₒ ⊗₁ U.id) U.∘ α⇒ U.∘ copy ⊗₁ U.id - ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ (refl⟩∘⟨ lemma₂) ⟩∘⟨refl ⟩ - fᵢ U.∘ U.id ⊗₁ ((gᵢ U.∘ U.id ⊗₁ term₂ U.∘ α⇒) U.∘ (fₒ ⊗₁ fₒ) ⊗₁ U.id U.∘ copy ⊗₁ U.id) U.∘ α⇒ U.∘ copy ⊗₁ U.id - ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ extendˡ U.assoc ⟩∘⟨refl ⟩ - fᵢ U.∘ U.id ⊗₁ ((gᵢ U.∘ U.id ⊗₁ term₂) U.∘ α⇒ U.∘ (fₒ ⊗₁ fₒ) ⊗₁ U.id U.∘ copy ⊗₁ U.id) U.∘ α⇒ U.∘ copy ⊗₁ U.id - ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ (refl⟩∘⟨ extendʳ assoc-commute-from ) ⟩∘⟨refl ⟩ - fᵢ U.∘ U.id ⊗₁ ((gᵢ U.∘ U.id ⊗₁ term₂) U.∘ fₒ ⊗₁ fₒ ⊗₁ U.id U.∘ α⇒ U.∘ copy ⊗₁ U.id) U.∘ α⇒ U.∘ copy ⊗₁ U.id - ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ U.assoc ⟩∘⟨refl ⟩ - fᵢ U.∘ U.id ⊗₁ (gᵢ U.∘ U.id ⊗₁ term₂ U.∘ fₒ ⊗₁ fₒ ⊗₁ U.id U.∘ α⇒ U.∘ copy ⊗₁ U.id) U.∘ α⇒ U.∘ copy ⊗₁ U.id - ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ (refl⟩∘⟨ pullˡ merge₂ˡ ) ⟩∘⟨refl ⟩ - fᵢ U.∘ U.id ⊗₁ (gᵢ U.∘ fₒ ⊗₁ (term₂ U.∘ fₒ ⊗₁ U.id) U.∘ α⇒ U.∘ copy ⊗₁ U.id) U.∘ α⇒ U.∘ copy ⊗₁ U.id - ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ (refl⟩∘⟨ refl⟩⊗⟨ pullʳ merge₁ʳ ⟩∘⟨refl) ⟩∘⟨refl ⟩ - fᵢ U.∘ U.id ⊗₁ (gᵢ U.∘ fₒ ⊗₁ term₁ U.∘ α⇒ U.∘ copy ⊗₁ U.id) U.∘ α⇒ U.∘ copy ⊗₁ U.id - ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ U.assoc ⟩∘⟨refl ⟨ - fᵢ U.∘ U.id ⊗₁ ((gᵢ U.∘ fₒ ⊗₁ term₁) U.∘ α⇒ U.∘ copy ⊗₁ U.id) U.∘ α⇒ U.∘ copy ⊗₁ U.id - ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ extendˡ U.assoc ⟩∘⟨refl ⟨ - fᵢ U.∘ U.id ⊗₁ ((gᵢ U.∘ fₒ ⊗₁ term₁ U.∘ α⇒) U.∘ copy ⊗₁ U.id) U.∘ α⇒ U.∘ copy ⊗₁ U.id - ≈⟨ refl⟩∘⟨ pushˡ split₂ʳ ⟩ - fᵢ U.∘ U.id ⊗₁ (gᵢ U.∘ fₒ ⊗₁ term₁ U.∘ α⇒) U.∘ U.id ⊗₁ copy ⊗₁ U.id U.∘ α⇒ U.∘ copy ⊗₁ U.id - ≈⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ assoc-commute-from ⟨ - fᵢ U.∘ U.id ⊗₁ (gᵢ U.∘ fₒ ⊗₁ term₁ U.∘ α⇒) U.∘ α⇒ U.∘ (U.id ⊗₁ copy) ⊗₁ U.id U.∘ copy ⊗₁ U.id - ≈⟨ refl⟩∘⟨ extendʳ (refl⟩⊗⟨ U.assoc ⟩∘⟨refl) ⟨ - fᵢ U.∘ U.id ⊗₁ ((gᵢ U.∘ fₒ ⊗₁ term₁) U.∘ α⇒) U.∘ α⇒ U.∘ (U.id ⊗₁ copy) ⊗₁ U.id U.∘ copy ⊗₁ U.id - ≈⟨ refl⟩∘⟨ pushˡ split₂ʳ ⟩ - fᵢ U.∘ U.id ⊗₁ (gᵢ U.∘ fₒ ⊗₁ term₁) U.∘ U.id ⊗₁ α⇒ U.∘ α⇒ U.∘ (U.id ⊗₁ copy) ⊗₁ U.id U.∘ copy ⊗₁ U.id - ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ insertˡ associator.isoʳ ⟩⊗⟨refl ⟩∘⟨refl ⟩ - fᵢ U.∘ U.id ⊗₁ (gᵢ U.∘ fₒ ⊗₁ term₁) U.∘ U.id ⊗₁ α⇒ U.∘ α⇒ U.∘ (α⇒ U.∘ α⇐ U.∘ U.id ⊗₁ copy) ⊗₁ U.id U.∘ copy ⊗₁ U.id - ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ split₁ʳ ⟩ - fᵢ U.∘ U.id ⊗₁ (gᵢ U.∘ fₒ ⊗₁ term₁) U.∘ U.id ⊗₁ α⇒ U.∘ α⇒ U.∘ α⇒ ⊗₁ U.id U.∘ (α⇐ U.∘ U.id ⊗₁ copy) ⊗₁ U.id U.∘ copy ⊗₁ U.id - ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ U.assoc ⟨ - fᵢ U.∘ U.id ⊗₁ (gᵢ U.∘ fₒ ⊗₁ term₁) U.∘ U.id ⊗₁ α⇒ U.∘ (α⇒ U.∘ α⇒ ⊗₁ U.id) U.∘ (α⇐ U.∘ U.id ⊗₁ copy) ⊗₁ U.id U.∘ copy ⊗₁ U.id - ≈⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ pentagon ⟩ - fᵢ U.∘ U.id ⊗₁ (gᵢ U.∘ fₒ ⊗₁ term₁) U.∘ α⇒ U.∘ α⇒ U.∘ (α⇐ U.∘ U.id ⊗₁ copy) ⊗₁ U.id U.∘ copy ⊗₁ U.id - ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ pushʳ serialize₁₂ ⟩∘⟨refl ⟩ - fᵢ U.∘ U.id ⊗₁ (term₃ U.∘ U.id ⊗₁ term₁) U.∘ α⇒ U.∘ α⇒ U.∘ (α⇐ U.∘ U.id ⊗₁ copy) ⊗₁ U.id U.∘ copy ⊗₁ U.id - ≈⟨ refl⟩∘⟨ pushˡ split₂ʳ ⟩ - fᵢ U.∘ U.id ⊗₁ term₃ U.∘ U.id ⊗₁ U.id ⊗₁ term₁ U.∘ α⇒ U.∘ α⇒ U.∘ (α⇐ U.∘ U.id ⊗₁ copy) ⊗₁ U.id U.∘ copy ⊗₁ U.id - ≈⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ assoc-commute-from ⟨ - fᵢ U.∘ U.id ⊗₁ term₃ U.∘ α⇒ U.∘ (U.id ⊗₁ U.id) ⊗₁ term₁ U.∘ α⇒ U.∘ (α⇐ U.∘ U.id ⊗₁ copy) ⊗₁ U.id U.∘ copy ⊗₁ U.id - ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ ⊗.identity ⟩⊗⟨refl ⟩∘⟨refl ⟩ - fᵢ U.∘ U.id ⊗₁ term₃ U.∘ α⇒ U.∘ U.id ⊗₁ term₁ U.∘ α⇒ U.∘ (α⇐ U.∘ U.id ⊗₁ copy) ⊗₁ U.id U.∘ copy ⊗₁ U.id - ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ lemma₁ ⟩ - fᵢ U.∘ U.id ⊗₁ term₃ U.∘ α⇒ U.∘ U.id ⊗₁ term₁ U.∘ copy ⊗₁ U.id U.∘ α⇒ U.∘ copy ⊗₁ U.id - ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ (U.Equiv.sym serialize₂₁ ○ serialize₁₂) ⟩ - fᵢ U.∘ U.id ⊗₁ term₃ U.∘ α⇒ U.∘ copy ⊗₁ U.id U.∘ U.id ⊗₁ term₁ U.∘ α⇒ U.∘ copy ⊗₁ U.id - ≈⟨ refl⟩∘⟨ refl⟩∘⟨ U.assoc ⟨ - fᵢ U.∘ U.id ⊗₁ term₃ U.∘ (α⇒ U.∘ copy ⊗₁ U.id) U.∘ U.id ⊗₁ term₁ U.∘ α⇒ U.∘ copy ⊗₁ U.id - ≈⟨ refl⟩∘⟨ U.assoc ⟨ - fᵢ U.∘ (U.id ⊗₁ term₃ U.∘ α⇒ U.∘ copy ⊗₁ U.id) U.∘ U.id ⊗₁ term₁ U.∘ α⇒ U.∘ copy ⊗₁ U.id - ≈⟨ U.assoc ⟨ - (fᵢ U.∘ U.id ⊗₁ term₃ U.∘ α⇒ U.∘ copy ⊗₁ U.id) U.∘ U.id ⊗₁ term₁ U.∘ α⇒ U.∘ copy ⊗₁ U.id ∎ - -identityˡ : {A B : Box} {f : WiringDiagram A B} → id ∘ f ≈ f -identityˡ {Aᵢ □ Aₒ} {Bᵢ □ Bₒ} {fᵢ ⧈ fₒ} = ≈ᵢ ⌸ U.identityˡ - where - open ⇒-Reasoning 𝒞 - open ⊗-Reasoning M - ≈ᵢ : fᵢ U.∘ U.id ⊗₁ ((λ⇒ U.∘ discard ⊗₁ U.id) U.∘ fₒ ⊗₁ U.id) U.∘ α⇒ U.∘ copy ⊗₁ U.id U.≈ fᵢ - ≈ᵢ = begin - fᵢ U.∘ U.id ⊗₁ ((λ⇒ U.∘ discard ⊗₁ U.id) U.∘ fₒ ⊗₁ U.id) U.∘ α⇒ U.∘ copy ⊗₁ U.id ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ pullʳ merge₁ʳ ⟩∘⟨refl ⟩ - fᵢ U.∘ U.id ⊗₁ (λ⇒ U.∘ (discard U.∘ fₒ) ⊗₁ U.id) U.∘ α⇒ U.∘ copy ⊗₁ U.id ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ (refl⟩∘⟨ η⇒ ⟩⊗⟨refl) ⟩∘⟨refl ⟩ - fᵢ U.∘ U.id ⊗₁ (λ⇒ U.∘ discard ⊗₁ U.id) U.∘ α⇒ U.∘ copy ⊗₁ U.id ≈⟨ refl⟩∘⟨ pushˡ split₂ʳ ⟩ - fᵢ U.∘ U.id ⊗₁ λ⇒ U.∘ U.id ⊗₁ discard ⊗₁ U.id U.∘ α⇒ U.∘ copy ⊗₁ U.id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ assoc-commute-from ⟨ - fᵢ U.∘ U.id ⊗₁ λ⇒ U.∘ α⇒ U.∘ (U.id ⊗₁ discard) ⊗₁ U.id U.∘ copy ⊗₁ U.id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ merge₁ˡ ⟩ - fᵢ U.∘ U.id ⊗₁ λ⇒ U.∘ α⇒ U.∘ (U.id ⊗₁ discard U.∘ copy) ⊗₁ U.id ≈⟨ refl⟩∘⟨ pullˡ triangle ⟩ - fᵢ U.∘ ρ⇒ ⊗₁ U.id U.∘ (U.id ⊗₁ discard U.∘ copy) ⊗₁ U.id ≈⟨ refl⟩∘⟨ merge₁ʳ ⟩ - fᵢ U.∘ (ρ⇒ U.∘ U.id ⊗₁ discard U.∘ copy) ⊗₁ U.id ≈⟨ refl⟩∘⟨ (refl⟩∘⟨ IsMonoid.identityʳ comonoid) ⟩⊗⟨refl ⟨ - fᵢ U.∘ (ρ⇒ U.∘ ρ⇐) ⊗₁ U.id ≈⟨ refl⟩∘⟨ unitorʳ.isoʳ ⟩⊗⟨refl ⟩ - fᵢ U.∘ U.id ⊗₁ U.id ≈⟨ elimʳ ⊗.identity ⟩ - fᵢ ∎ - -identityʳ : {A B : Box} {f : WiringDiagram A B} → (f ∘ id) ≈ f -identityʳ {Aᵢ □ Aₒ} {Bᵢ □ Bₒ} {fᵢ ⧈ fₒ} = ≈ᵢ ⌸ U.identityʳ - where - open ⇒-Reasoning 𝒞 - open ⊗-Reasoning M - ≈ᵢ : (λ⇒ U.∘ discard ⊗₁ U.id) U.∘ U.id ⊗₁ (fᵢ U.∘ U.id ⊗₁ U.id) U.∘ α⇒ U.∘ copy ⊗₁ U.id U.≈ fᵢ - ≈ᵢ = begin - (λ⇒ U.∘ discard ⊗₁ U.id) U.∘ U.id ⊗₁ (fᵢ U.∘ U.id ⊗₁ U.id) U.∘ α⇒ U.∘ copy ⊗₁ U.id ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ elimʳ ⊗.identity ⟩∘⟨refl ⟩ - (λ⇒ U.∘ discard ⊗₁ U.id) U.∘ U.id ⊗₁ fᵢ U.∘ α⇒ U.∘ copy ⊗₁ U.id ≈⟨ pullˡ (pullʳ (U.Equiv.sym serialize₁₂)) ⟩ - (λ⇒ U.∘ discard ⊗₁ fᵢ) U.∘ α⇒ U.∘ copy ⊗₁ U.id ≈⟨ pullʳ (pushˡ serialize₂₁) ⟩ - λ⇒ U.∘ U.id ⊗₁ fᵢ U.∘ discard ⊗₁ U.id U.∘ α⇒ U.∘ copy ⊗₁ U.id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩⊗⟨ ⊗.identity ⟩∘⟨refl ⟨ - λ⇒ U.∘ U.id ⊗₁ fᵢ U.∘ discard ⊗₁ U.id ⊗₁ U.id U.∘ α⇒ U.∘ copy ⊗₁ U.id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ assoc-commute-from ⟨ - λ⇒ U.∘ U.id ⊗₁ fᵢ U.∘ α⇒ U.∘ (discard ⊗₁ U.id) ⊗₁ U.id U.∘ copy ⊗₁ U.id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ merge₁ʳ ⟩ - λ⇒ U.∘ U.id ⊗₁ fᵢ U.∘ α⇒ U.∘ (discard ⊗₁ U.id U.∘ copy) ⊗₁ U.id ≈⟨ extendʳ unitorˡ-commute-from ⟩ - fᵢ U.∘ λ⇒ U.∘ α⇒ U.∘ (discard ⊗₁ U.id U.∘ copy) ⊗₁ U.id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ IsMonoid.identityˡ comonoid ⟩⊗⟨refl ⟨ - fᵢ U.∘ λ⇒ U.∘ α⇒ U.∘ λ⇐ ⊗₁ U.id ≈⟨ refl⟩∘⟨ pullˡ coherence₁ ⟩ - fᵢ U.∘ λ⇒ ⊗₁ U.id U.∘ λ⇐ ⊗₁ U.id ≈⟨ refl⟩∘⟨ merge₁ʳ ⟩ - fᵢ U.∘ (λ⇒ U.∘ λ⇐) ⊗₁ U.id ≈⟨ refl⟩∘⟨ unitorˡ.isoʳ ⟩⊗⟨refl ⟩ - fᵢ U.∘ U.id ⊗₁ U.id ≈⟨ elimʳ ⊗.identity ⟩ - fᵢ ∎ - -WD : Category o ℓ e -WD = categoryHelper record - { Obj = Box - ; _⇒_ = WiringDiagram - ; _≈_ = _≈_ - ; id = id - ; _∘_ = _∘_ - ; assoc = assoc - ; identityˡ = identityˡ - ; identityʳ = identityʳ - ; equiv = ≈-isEquiv - ; ∘-resp-≈ = ∘-resp-≈ - } |