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
|
{-# OPTIONS --without-K --safe #-}
open import Categories.Category using (Category)
open import Category.Dagger.Semiadditive using (SemiadditiveDagger; IdempotentSemiadditiveDagger)
open import Level using (Level)
module Data.WiringDiagram.Equalities {o ℓ e : Level} {𝒞 : Category o ℓ e} (S : IdempotentSemiadditiveDagger 𝒞) where
module S = IdempotentSemiadditiveDagger S
import Categories.Morphism.Reasoning 𝒞 as ⇒-Reasoning
open import Categories.Category.Monoidal using (module Monoidal)
open import Categories.Category.Monoidal.Utilities using (module Shorthands)
open import Data.WiringDiagram.Core S.semiadditiveDagger using (_⌸_; _⌻_; _≈-⧈_; ≈-trans; loop; push; pull; merge; split)
open Category 𝒞
open Equiv
open HomReasoning
open IdempotentSemiadditiveDagger S
open ⇒-Reasoning
⟨π₁,id⟩ : {A B : Obj} → ⟨ π₁ {A} {B} , id ⟩ ≈ assocˡ ∘ Δ ×₁ id
⟨π₁,id⟩ = begin
⟨ π₁ , id ⟩ ≈⟨ ⟨⟩-congˡ η ⟨
⟨ π₁ , ⟨ π₁ , π₂ ⟩ ⟩ ≈⟨ assocˡ∘⟨⟩ ⟨
assocˡ ∘ ⟨ ⟨ π₁ , π₁ ⟩ , π₂ ⟩ ≈⟨ refl⟩∘⟨ ⟨⟩-cong₂ Δ∘ identityˡ ⟨
assocˡ ∘ Δ ×₁ id ∎
loop∘loop : {A : Obj} → loop ⌻ loop ≈-⧈ loop {A}
loop∘loop {A} = ≈ᵢ ⌸ identity²
where
≈ᵢ : ∇ ∘ ⟨ π₁ , (∇ ∘ id ×₁ id) ⟩ ≈ ∇
≈ᵢ = begin
∇ ∘ ⟨ π₁ , ∇ ∘ id ×₁ id ⟩ ≈⟨ refl⟩∘⟨ ⟨⟩-cong₂ (sym identityˡ) (refl⟩∘⟨ id×₁id) ⟩
∇ ∘ ⟨ id ∘ π₁ , ∇ ∘ id ⟩ ≈⟨ refl⟩∘⟨ ×₁∘⟨⟩ ⟨
∇ ∘ id ×₁ ∇ ∘ ⟨ π₁ , id ⟩ ≈⟨ refl⟩∘⟨ pushʳ ⟨π₁,id⟩ ⟩
∇ ∘ (id ×₁ ∇ ∘ assocˡ) ∘ Δ ×₁ id ≈⟨ extendʳ ∇-assoc-×₁ ⟨
∇ ∘ ∇ ×₁ id ∘ Δ ×₁ id ≈⟨ refl⟩∘⟨ first∘first ⟩
∇ ∘ (∇ ∘ Δ) ×₁ id ≈⟨ refl⟩∘⟨ first-cong ∇∘Δ ⟩
∇ ∘ id ×₁ id ≈⟨ elimʳ id×₁id ⟩
∇ ∎
loop∘push∘loop≈merge : {A B : Obj} (f : A ⇒ B) → id ≤ ((f †) ∘ f) → loop ⌻ push f ⌻ loop ≈-⧈ merge f
loop∘push∘loop≈merge f id≤f†∘f = ≈ᵢ ⌸ (identityˡ ○ identityʳ)
where
≈ᵢ : (∇ ∘ ⟨ π₁ , (f † ∘ π₂) ∘ id ×₁ id ⟩) ∘ ⟨ π₁ , ∇ ∘ (f ∘ id) ×₁ id ⟩
≈ f † ∘ ∇ ∘ f ×₁ id
≈ᵢ = begin
(∇ ∘ ⟨ π₁ , (f † ∘ π₂) ∘ id ×₁ id ⟩) ∘ ⟨ π₁ , ∇ ∘ (f ∘ id) ×₁ id ⟩ ≈⟨ pullʳ (⟨⟩-congˡ (elimʳ id×₁id) ⟩∘⟨ ⟨⟩-congˡ (refl⟩∘⟨ first-cong identityʳ)) ⟩
∇ ∘ ⟨ π₁ , f † ∘ π₂ ⟩ ∘ ⟨ π₁ , ∇ ∘ f ×₁ id ⟩ ≈⟨ refl⟩∘⟨ ⟨⟩∘ ⟩
∇ ∘ ⟨ π₁ ∘ ⟨ π₁ , ∇ ∘ f ×₁ id ⟩ , (f † ∘ π₂) ∘ ⟨ π₁ , ∇ ∘ f ×₁ id ⟩ ⟩ ≈⟨ refl⟩∘⟨ ⟨⟩-cong₂ project₁ (pullʳ project₂) ⟩
∇ ∘ ⟨ π₁ , f † ∘ ∇ ∘ f ×₁ id ⟩ ≈⟨ refl⟩∘⟨ ⟨⟩-congˡ (extendʳ ⇒∇-×₁) ⟩
∇ ∘ ⟨ π₁ , ∇ ∘ (f †) ×₁ (f †) ∘ f ×₁ id ⟩ ≈⟨ refl⟩∘⟨ ⟨⟩-congˡ (refl⟩∘⟨ ×₁∘first) ⟩
∇ ∘ ⟨ π₁ , ∇ ∘ (f † ∘ f) ×₁ (f †) ⟩ ≈⟨ refl⟩∘⟨ second∘⟨⟩ ⟨
∇ ∘ id ×₁ ∇ ∘ ⟨ π₁ , (f † ∘ f) ×₁ (f †) ⟩ ≈⟨ refl⟩∘⟨ pushʳ (sym assocˡ∘⟨⟩) ⟩
∇ ∘ (id ×₁ ∇ ∘ assocˡ) ∘ ⟨ ⟨ π₁ , (f † ∘ f) ∘ π₁ ⟩ , f † ∘ π₂ ⟩ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⟨⟩-congʳ (⟨⟩-congʳ identityˡ) ⟨
∇ ∘ (id ×₁ ∇ ∘ assocˡ) ∘ ⟨ ⟨ id ∘ π₁ , (f † ∘ f) ∘ π₁ ⟩ , f † ∘ π₂ ⟩ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⟨⟩-congʳ ⟨⟩∘ ⟨
∇ ∘ (id ×₁ ∇ ∘ assocˡ) ∘ ⟨ id , f † ∘ f ⟩ ×₁ (f †) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ×₁-congʳ ×₁∘Δ ⟨
∇ ∘ (id ×₁ ∇ ∘ assocˡ) ∘ (id ×₁ (f † ∘ f) ∘ Δ) ×₁ (f †) ≈⟨ extendʳ ∇-assoc-×₁ ⟨
∇ ∘ (∇ ×₁ id) ∘ (id ×₁ (f † ∘ f) ∘ Δ) ×₁ (f †) ≈⟨ refl⟩∘⟨ first∘×₁ ⟩
∇ ∘ (id + (f † ∘ f)) ×₁ (f †) ≈⟨ refl⟩∘⟨ ×₁-congʳ id≤f†∘f ⟩
∇ ∘ (f † ∘ f) ×₁ (f †) ≈⟨ refl⟩∘⟨ ×₁∘first ⟨
∇ ∘ (f †) ×₁ (f †) ∘ f ×₁ id ≈⟨ extendʳ ⇒∇-×₁ ⟨
f † ∘ ∇ ∘ f ×₁ id ∎
merge≈loop∘push : {A B : Obj} (f : A ⇒ B) → merge f ≈-⧈ loop ⌻ push f
merge≈loop∘push f = ≈ᵢ ⌸ Equiv.sym identityˡ
where
≈ᵢ : f † ∘ ∇ ∘ f ×₁ id ≈ (f † ∘ π₂) ∘ ⟨ π₁ , ∇ ∘ f ×₁ id ⟩
≈ᵢ = begin
f † ∘ ∇ ∘ f ×₁ id ≈⟨ pushʳ (sym project₂) ⟩
(f † ∘ π₂) ∘ ⟨ π₁ , ∇ ∘ f ×₁ id ⟩ ∎
loop∘pull∘loop≈split : {A B : Obj} (f : A ⇒ B) → (f ∘ (f †)) ≤ id → loop ⌻ pull f ⌻ loop ≈-⧈ split f
loop∘pull∘loop≈split f f∘f†≤id = ≈ᵢ ⌸ (identityˡ ○ identityʳ)
where
≈ᵢ : (∇ ∘ ⟨ π₁ , (f ∘ π₂) ∘ id ×₁ id ⟩) ∘ ⟨ π₁ , ∇ ∘ (f † ∘ id) ×₁ id ⟩ ≈ ∇ ∘ id ×₁ f
≈ᵢ = begin
(∇ ∘ ⟨ π₁ , (f ∘ π₂) ∘ id ×₁ id ⟩) ∘ ⟨ π₁ , ∇ ∘ (f † ∘ id) ×₁ id ⟩ ≈⟨ pullʳ (⟨⟩-congˡ (elimʳ id×₁id) ⟩∘⟨ ⟨⟩-congˡ (refl⟩∘⟨ first-cong identityʳ)) ⟩
∇ ∘ ⟨ π₁ , (f ∘ π₂) ⟩ ∘ ⟨ π₁ , ∇ ∘ (f †) ×₁ id ⟩ ≈⟨ refl⟩∘⟨ ⟨⟩∘ ⟩
∇ ∘ ⟨ π₁ ∘ ⟨ π₁ , ∇ ∘ (f †) ×₁ id ⟩ , (f ∘ π₂) ∘ ⟨ π₁ , ∇ ∘ (f †) ×₁ id ⟩ ⟩ ≈⟨ refl⟩∘⟨ ⟨⟩-cong₂ project₁ (pullʳ project₂) ⟩
∇ ∘ ⟨ π₁ , f ∘ ∇ ∘ (f †) ×₁ id ⟩ ≈⟨ refl⟩∘⟨ ⟨⟩-congˡ (extendʳ ⇒∇-×₁) ⟩
∇ ∘ ⟨ π₁ , ∇ ∘ f ×₁ f ∘ (f †) ×₁ id ⟩ ≈⟨ refl⟩∘⟨ ⟨⟩-congˡ (refl⟩∘⟨ ×₁∘first) ⟩
∇ ∘ ⟨ π₁ , ∇ ∘ (f ∘ f †) ×₁ f ⟩ ≈⟨ refl⟩∘⟨ ⟨⟩-congˡ identityʳ ⟨
∇ ∘ ⟨ π₁ , (∇ ∘ (f ∘ f †) ×₁ f) ∘ id ⟩ ≈⟨ refl⟩∘⟨ second∘⟨⟩ ⟨
∇ ∘ id ×₁ (∇ ∘ (f ∘ f †) ×₁ f) ∘ ⟨ π₁ , id ⟩ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⟨⟩-congˡ η ⟨
∇ ∘ id ×₁ (∇ ∘ (f ∘ f †) ×₁ f) ∘ ⟨ π₁ , ⟨ π₁ , π₂ ⟩ ⟩ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ assocˡ∘⟨⟩ ⟨
∇ ∘ id ×₁ (∇ ∘ (f ∘ f †) ×₁ f) ∘ assocˡ ∘ ⟨ ⟨ π₁ , π₁ ⟩ , π₂ ⟩ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ ⟨⟩-cong₂ Δ∘ identityˡ ⟨
∇ ∘ id ×₁ (∇ ∘ (f ∘ f †) ×₁ f) ∘ assocˡ ∘ Δ ×₁ id ≈⟨ refl⟩∘⟨ pushˡ (sym second∘×₁) ⟩
∇ ∘ id ×₁ ∇ ∘ id ×₁ (f ∘ f †) ×₁ f ∘ assocˡ ∘ Δ ×₁ id ≈⟨ refl⟩∘⟨ pushʳ (extendʳ (sym assocˡ∘×₁)) ⟩
∇ ∘ (id ×₁ ∇ ∘ assocˡ) ∘ (id ×₁ (f ∘ f †)) ×₁ f ∘ Δ ×₁ id ≈⟨ extendʳ ∇-assoc-×₁ ⟨
∇ ∘ ∇ ×₁ id ∘ (id ×₁ (f ∘ f †)) ×₁ f ∘ Δ ×₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ×₁∘first ⟩
∇ ∘ ∇ ×₁ id ∘ (id ×₁ (f ∘ f †) ∘ Δ) ×₁ f ≈⟨ refl⟩∘⟨ first∘×₁ ⟩
∇ ∘ (id + (f ∘ f †)) ×₁ f ≈⟨ refl⟩∘⟨ ×₁-congʳ (+-comm id (f ∘ f †)) ⟩
∇ ∘ ((f ∘ f †) + id) ×₁ f ≈⟨ refl⟩∘⟨ ×₁-congʳ f∘f†≤id ⟩
∇ ∘ id ×₁ f ∎
split≈pull∘loop : {A B : Obj} (f : A ⇒ B) → split f ≈-⧈ pull f ⌻ loop
split≈pull∘loop f = ≈ᵢ ⌸ Equiv.sym identityʳ
where
≈ᵢ : ∇ ∘ id ×₁ f
≈ ∇ ∘ ⟨ π₁ , (f ∘ π₂) ∘ id ×₁ id ⟩
≈ᵢ = begin
∇ ∘ id ×₁ f ≈⟨ refl⟩∘⟨ ⟨⟩-congʳ identityˡ ⟩
∇ ∘ ⟨ π₁ , f ∘ π₂ ⟩ ≈⟨ refl⟩∘⟨ ⟨⟩-congˡ (introʳ id×₁id) ⟩
∇ ∘ ⟨ π₁ , (f ∘ π₂) ∘ id ×₁ id ⟩ ∎
loop∘push∘loop : {A B : Obj} (f : A ⇒ B) → id ≤ ((f †) ∘ f) → loop ⌻ push f ⌻ loop ≈-⧈ loop ⌻ push f
loop∘push∘loop f id≤f†∘f = ≈-trans (loop∘push∘loop≈merge f id≤f†∘f) (merge≈loop∘push f)
loop∘pull∘loop : {A B : Obj} → (f : A ⇒ B) → (f ∘ (f †)) ≤ id → loop ⌻ pull f ⌻ loop ≈-⧈ pull f ⌻ loop
loop∘pull∘loop f f∘f†≤id = ≈-trans (loop∘pull∘loop≈split f f∘f†≤id) (split≈pull∘loop f)
|
