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
|
{-# OPTIONS --without-K --safe #-}
open import Categories.Category using (Category)
open import Category.Dagger.Semiadditive using (SemiadditiveDagger)
open import Level using (Level)
module Data.WiringDiagram.Directed
{o ℓ e : Level}
{𝒞 : Category o ℓ e}
(S : SemiadditiveDagger 𝒞)
where
import Categories.Morphism.Reasoning 𝒞 as ⇒-Reasoning
open import Categories.Category.Helper using (categoryHelper)
open import Categories.Category.Monoidal using (Monoidal)
open import Categories.Category.Monoidal.Utilities using (module Shorthands)
open import Categories.Functor.Bifunctor using (Bifunctor)
open import Data.Product using (_,_)
open import Data.WiringDiagram.Core S using (Box; WiringDiagram; _≈-⧈_; _□_; _⧈_; _⌸_; id-⧈; _⌻_; ≈-isEquiv; pulsh)
open Category 𝒞
open SemiadditiveDagger S
private
⌻-resp-≈ : {A B C : Box} {f h : WiringDiagram B C} {g i : WiringDiagram A B} → f ≈-⧈ h → g ≈-⧈ i → f ⌻ g ≈-⧈ h ⌻ i
⌻-resp-≈ {A} {B} {C} {fᵢ ⧈ fₒ} {hᵢ ⧈ hₒ} {gᵢ ⧈ gₒ} {iᵢ ⧈ iₒ} (fᵢ≈hᵢ ⌸ fₒ≈hₒ) (gᵢ≈iᵢ ⌸ gₒ≈iₒ) = ≈ᵢ ⌸ ∘-resp-≈ fₒ≈hₒ gₒ≈iₒ
where
open HomReasoning
≈ᵢ : gᵢ ∘ ⟨ π₁ , fᵢ ∘ gₒ ×₁ id ⟩
≈ iᵢ ∘ ⟨ π₁ , hᵢ ∘ iₒ ×₁ id ⟩
≈ᵢ = gᵢ≈iᵢ ⟩∘⟨ ⟨⟩-congˡ (fᵢ≈hᵢ ⟩∘⟨ first-cong gₒ≈iₒ)
⌻-assoc : {A B C D : Box} {f : WiringDiagram A B} {g : WiringDiagram B C} {h : WiringDiagram C D} → (h ⌻ g) ⌻ f ≈-⧈ h ⌻ (g ⌻ f)
⌻-assoc {Aᵢ □ Aₒ} {Bᵢ □ Bₒ} {Cᵢ □ Cₒ} {Dᵢ □ Dₒ} {fᵢ ⧈ fₒ} {gᵢ ⧈ gₒ} {hᵢ ⧈ hₒ} = ≈ᵢ ⌸ assoc
where
open HomReasoning
open ⇒-Reasoning
open Equiv
≈ᵢ : fᵢ ∘ ⟨ π₁ , (gᵢ ∘ ⟨ π₁ , hᵢ ∘ gₒ ×₁ id ⟩) ∘ fₒ ×₁ id ⟩
≈ (fᵢ ∘ ⟨ π₁ , gᵢ ∘ fₒ ×₁ id ⟩) ∘ ⟨ π₁ , hᵢ ∘ (gₒ ∘ fₒ) ×₁ id ⟩
≈ᵢ = begin
fᵢ ∘ ⟨ π₁ , (gᵢ ∘ ⟨ π₁ , hᵢ ∘ gₒ ×₁ id ⟩) ∘ fₒ ×₁ id ⟩ ≈⟨ refl⟩∘⟨ ⟨⟩-congˡ (pullʳ ⟨⟩∘) ⟩
fᵢ ∘ ⟨ π₁ , gᵢ ∘ ⟨ π₁ ∘ fₒ ×₁ id , (hᵢ ∘ gₒ ×₁ id) ∘ fₒ ×₁ id ⟩ ⟩ ≈⟨ refl⟩∘⟨ ⟨⟩-congˡ (refl⟩∘⟨ ⟨⟩-cong₂ π₁∘×₁ (pullʳ first∘first)) ⟩
fᵢ ∘ ⟨ π₁ , gᵢ ∘ ⟨ fₒ ∘ π₁ , hᵢ ∘ (gₒ ∘ fₒ) ×₁ id ⟩ ⟩ ≈⟨ refl⟩∘⟨ ⟨⟩-cong₂ project₁ (pullʳ first∘⟨⟩) ⟨
fᵢ ∘ ⟨ π₁ ∘ ⟨ π₁ , _ ⟩ , (gᵢ ∘ fₒ ×₁ id) ∘ ⟨ π₁ , _ ⟩ ⟩ ≈⟨ pushʳ (sym ⟨⟩∘) ⟩
(fᵢ ∘ ⟨ π₁ , gᵢ ∘ fₒ ×₁ id ⟩) ∘ ⟨ π₁ , hᵢ ∘ (gₒ ∘ fₒ) ×₁ id ⟩ ∎
⌻-identityˡ : {A B : Box} {f : WiringDiagram A B} → id-⧈ ⌻ f ≈-⧈ f
⌻-identityˡ {Aᵢ □ Aₒ} {Bᵢ □ Bₒ} {fᵢ ⧈ fₒ} = ≈ᵢ ⌸ identityˡ
where
open HomReasoning
open ⇒-Reasoning
≈ᵢ : fᵢ ∘ ⟨ π₁ , π₂ ∘ fₒ ×₁ id ⟩ ≈ fᵢ
≈ᵢ = begin
fᵢ ∘ ⟨ π₁ , π₂ ∘ fₒ ×₁ id ⟩ ≈⟨ refl⟩∘⟨ ⟨⟩-congˡ π₂∘first ⟩
fᵢ ∘ ⟨ π₁ , π₂ ⟩ ≈⟨ elimʳ η ⟩
fᵢ ∎
⌻-identityʳ : {A B : Box} {f : WiringDiagram A B} → f ⌻ id-⧈ ≈-⧈ f
⌻-identityʳ {Aᵢ □ Aₒ} {Bᵢ □ Bₒ} {fᵢ ⧈ fₒ} = ≈ᵢ ⌸ identityʳ
where
open HomReasoning
open ⇒-Reasoning
≈ᵢ : π₂ ∘ ⟨ π₁ , fᵢ ∘ id ×₁ id ⟩ ≈ fᵢ
≈ᵢ = begin
π₂ ∘ ⟨ π₁ , fᵢ ∘ id ×₁ id ⟩ ≈⟨ project₂ ⟩
fᵢ ∘ id ×₁ id ≈⟨ elimʳ id×₁id ⟩
fᵢ ∎
-- The category of directed wiring diagrams
DWD : Category o ℓ e
DWD = categoryHelper record
{ Obj = Box
; _⇒_ = WiringDiagram
; _≈_ = _≈-⧈_
; id = id-⧈
; _∘_ = _⌻_
; assoc = ⌻-assoc
; identityˡ = ⌻-identityˡ
; identityʳ = ⌻-identityʳ
; equiv = ≈-isEquiv
; ∘-resp-≈ = ⌻-resp-≈
}
-- Every pair of morphisms in 𝒞 gives a wiring diagram
Pulsh : Bifunctor op 𝒞 DWD
Pulsh = record
{ F₀ = λ (A , B) → A □ B
; F₁ = λ (f , g) → pulsh f g
; identity = elimˡ Equiv.refl ⌸ Equiv.refl
; homomorphism = λ { {A} {B} {C} {f , g} {f′ , g′} → homoᵢ g g′ f f′ ⌸ Equiv.refl }
; F-resp-≈ = λ (f≈f′ , g≈g′) → (f≈f′ ⟩∘⟨refl) ⌸ g≈g′
}
where
open HomReasoning
open ⇒-Reasoning
open Equiv
homoᵢ
: {A B C D E F : Obj} (g : A ⇒ B) (g′ : B ⇒ C) (f : E ⇒ F) (f′ : D ⇒ E)
→ (f ∘ f′) ∘ π₂ ≈ (f ∘ π₂) ∘ ⟨ π₁ , (f′ ∘ π₂) ∘ g ×₁ id ⟩
homoᵢ g g′ f f′ = begin
(f ∘ f′) ∘ π₂ ≈⟨ pullʳ (pushʳ (sym π₂∘first)) ⟩
f ∘ (f′ ∘ π₂) ∘ g ×₁ id ≈⟨ pushʳ (sym project₂) ⟩
(f ∘ π₂) ∘ ⟨ π₁ , (f′ ∘ π₂) ∘ g ×₁ id ⟩ ∎
|
