From 66bdd7123027650ada325a3a2e3641b0a0ce375c Mon Sep 17 00:00:00 2001 From: Jacques Comeaux Date: Sat, 14 Mar 2026 17:39:03 -0500 Subject: Add wiring diagram equalities --- Data/WiringDiagram/Core.agda | 20 ++++++++++++++++++-- 1 file changed, 18 insertions(+), 2 deletions(-) (limited to 'Data/WiringDiagram/Core.agda') 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 † -- cgit v1.2.3