blob: 2af7cb6e333ba34264db1e38f733d932cc9d23bb (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
|
{-# 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
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; 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)
open Category 𝒞
module DWD = Category DWD
-- The category of balanced wiring diagrams
BWD : Category o ℓ e
BWD = record
{ Obj = Obj
; _⇒_ = λ A B → WiringDiagram (A □ A) (B □ B)
; DWD
}
-- Inclusion functor from BWD to DWD
Include : Functor BWD DWD
Include = record
{ F₀ = λ A → A □ A
; F₁ = idf
; identity = DWD.Equiv.refl
; homomorphism = DWD.Equiv.refl
; F-resp-≈ = idf
}
-- 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 → (⟨ 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 : 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 ∎
-- 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 ∎
|
