Add pull functor from relations to wiring diagrams

1 files changed, 48 insertions, 10 deletions

diff --git a/Data/WiringDiagram/Balanced.agda b/Data/WiringDiagram/Balanced.agda
index ada297b..2af7cb6 100644
--- a/Data/WiringDiagram/Balanced.agda
+++ b/Data/WiringDiagram/Balanced.agda
@@ -14,19 +14,19 @@ 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; _□_; _⌸_; push)
+open import Data.WiringDiagram.Core S using (WiringDiagram; _□_; _⌸_; push; pull)
 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 () renaming (id to idf)
 
-module 𝒞 = Category 𝒞
+open 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)
     ; DWD
     }
@@ -36,12 +36,10 @@ Include : Functor BWD DWD
 Include = record
     { F₀ = λ A → A □ A
     ; F₁ = idf
-    ; identity = Equiv.refl
-    ; homomorphism = Equiv.refl
+    ; identity = DWD.Equiv.refl
+    ; homomorphism = DWD.Equiv.refl
     ; F-resp-≈ = idf
     }
-  where
-    open DWD using (module Equiv)
 
 -- Covariant functor from underlying category to BWD
 Push : Functor 𝒞 BWD
@@ -50,12 +48,11 @@ Push = record
     ; 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
+    ; F-resp-≈ = λ f≈g → (⟨ f≈g ⟩† ⟩∘⟨refl) ⌸ f≈g
     }
   where
-    open Category 𝒞
     open IdempotentSemiadditiveDagger S
-      using (+-monoidal; _†; p₂; _⊕₁_; △; !; p₁; p₂-⊕; ⇒!; ⇒△; ρ⇒≈p₁; p₁∘△; †-homomorphism; †-identity; †-resp-≈)
+      using (+-monoidal; _†; p₂; _⊕₁_; △; !; p₁; p₂-⊕; ⇒!; ⇒△; ρ⇒≈p₁; p₁∘△; †-homomorphism; †-identity; ⟨_⟩†)
     open Monoidal +-monoidal using (assoc-commute-from; unitorˡ-commute-from; triangle)
     open Shorthands +-monoidal using (α⇒; λ⇒; ρ⇒)
     open ⇒-Reasoning 𝒞
@@ -85,3 +82,44 @@ Push = record
         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              ∎
+
+-- Contravariant functor from underlying category to BWD
+Pull : Functor op BWD
+Pull = record
+    { F₀ = idf
+    ; F₁ = pull
+    ; identity = identityˡ ⌸ †-identity
+    ; homomorphism = λ {A B C f g} → homoᵢ f g ⌸ †-homomorphism
+    ; F-resp-≈ = λ f≈g → (f≈g ⟩∘⟨refl) ⌸ ⟨ f≈g ⟩†
+    }
+  where
+    open IdempotentSemiadditiveDagger S
+      using (+-monoidal; _†; p₂; _⊕₁_; △; !; p₁; p₂-⊕; ⇒!; ⇒△; ρ⇒≈p₁; p₁∘△; †-homomorphism; †-identity; ⟨_⟩†)
+    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 : B ⇒ A)
+          (g : C ⇒ B)
+        → (f ∘ g) ∘ p₂
+        ≈ (f ∘ p₂) ∘ id ⊕₁ ((g ∘ p₂) ∘ (f †) ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id
+    homoᵢ f g = begin
+        (f ∘ g) ∘ p₂                                                          ≈⟨ pullʳ (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              ∎