diff options
Diffstat (limited to 'Data/WiringDiagram/Core.agda')
| -rw-r--r-- | Data/WiringDiagram/Core.agda | 20 |
1 files changed, 18 insertions, 2 deletions
diff --git a/Data/WiringDiagram/Core.agda b/Data/WiringDiagram/Core.agda index d2e01cd..9903ce5 100644 --- a/Data/WiringDiagram/Core.agda +++ b/Data/WiringDiagram/Core.agda @@ -14,7 +14,7 @@ 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 IdempotentSemiadditiveDagger S using (_⊕₀_; _⊕₁_; p₂; +-monoidal; △; ▽; _†) open Shorthands +-monoidal using (α⇒) -- A "Box" is a pair of objects from the underlying category, @@ -125,6 +125,22 @@ _⌻_ {Aᵢ □ Aₒ} {Bᵢ □ Bₒ} {Cᵢ □ Cₒ} (f′ ⧈ g′) (f ⧈ g) infixr 9 _⌻_ --- The loop wiring diagram +-- Special wiring diagrams + loop : {A : Obj} → WiringDiagram (A □ A) (A □ A) loop = ▽ ⧈ id + +pulsh : {A B C D : Obj} → A ⇒ B → C ⇒ D → WiringDiagram (B □ C) (A □ D) +pulsh f g = f ∘ p₂ ⧈ g + +push : {A B : Obj} → A ⇒ B → WiringDiagram (A □ A) (B □ B) +push f = pulsh (f †) f + +pull : {A B : Obj} → A ⇒ B → WiringDiagram (B □ B) (A □ A) +pull f = pulsh f (f †) + +merge : {A B : Obj} → A ⇒ B → WiringDiagram (A □ A) (B □ B) +merge f = f † ∘ ▽ ∘ f ⊕₁ id ⧈ f + +split : {A B : Obj} → A ⇒ B → WiringDiagram (B □ B) (A □ A) +split f = ▽ ∘ id ⊕₁ f ⧈ f † |