blob: 3698a60e3e3541967aaf2fa1c94d4b9fffe7592c (
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
|
{-# OPTIONS --without-K --safe #-}
open import Categories.Category using (Category)
open import Categories.Functor using (Functor; _∘F_)
open import Category.Dagger.Semiadditive using (IdempotentSemiadditiveDagger)
open import Data.WiringDiagram.Balanced using (BWD)
open import Level using (Level)
open import Category.KaroubiComplete using (KaroubiComplete)
module Data.WiringDiagram.Looped
{o ℓ e o′ ℓ′ e′ : Level}
{𝒞 : Category o ℓ e}
{𝒟 : Category o′ ℓ′ e′}
{S : IdempotentSemiadditiveDagger 𝒞}
(karoubiComplete : KaroubiComplete 𝒟)
(F : Functor (BWD S) 𝒟)
where
open import Categories.Functor.Properties using ([_]-resp-∘)
open import Category.Dagger.2-Poset using (Dagger-2-Poset; dagger-2-poset; Maps; Map)
open import Data.WiringDiagram.Balanced S using (Include; Push)
open import Data.WiringDiagram.Core S using (loop; id-⧈; _□_)
open import Data.WiringDiagram.Equalities S using (loop∘loop; loop∘push∘loop)
module 𝒞 = Category 𝒞
module 𝒟 = Category 𝒟
module BWD = Category (BWD S)
module F = Functor F
open import Categories.Morphism.Idempotent 𝒟 using (IsSplitIdempotent)
module _ (A : 𝒞.Obj) where
open KaroubiComplete karoubiComplete using (split)
open IsSplitIdempotent (split ([ F ]-resp-∘ (loop∘loop {A})))
Unlooped Looped : 𝒟.Obj
Unlooped = F.₀ A
Looped = obj
L : Unlooped 𝒟.⇒ Unlooped
L = F.₁ loop
π : Unlooped 𝒟.⇒ Looped
π = retract
forget : Looped 𝒟.⇒ Unlooped
forget = section
forget∘π : forget 𝒟.∘ π 𝒟.≈ L
forget∘π = splits
π∘forget : π 𝒟.∘ forget 𝒟.≈ 𝒟.id
π∘forget = retracts
π∘l : π 𝒟.∘ L 𝒟.≈ π
π∘l = retract-absorb
module Push = Functor Push
S′ : Dagger-2-Poset
S′ = dagger-2-poset S
Merge : Functor (Maps S′) 𝒟
Merge = record
{ F₀ = Looped
; F₁ = λ {A} {B} f → π B ∘ F.₁ (Push.₁ (map f)) ∘ forget A
; identity = iden
; homomorphism = λ {f = f} {g} → homo {f = f} {g}
; F-resp-≈ = resp
}
where
open Map
open Category 𝒟 using (_∘_)
open 𝒟.HomReasoning
import Categories.Morphism.Reasoning as ⇒-Reasoning
open ⇒-Reasoning 𝒟
iden : {A : 𝒞.Obj} → π A ∘ F.₁ (Push.₁ 𝒞.id) ∘ forget A 𝒟.≈ 𝒟.id
iden {A} = begin
π A ∘ F.₁ (Push.₁ 𝒞.id) ∘ forget A ≈⟨ refl⟩∘⟨ F.F-resp-≈ Push.identity ⟩∘⟨refl ⟩
π A ∘ F.₁ BWD.id ∘ forget A ≈⟨ refl⟩∘⟨ elimˡ F.identity ⟩
π A ∘ forget A ≈⟨ π∘forget A ⟩
𝒟.id ∎
homo
: {X Y Z : 𝒞.Obj}
{f : Map S′ X Y}
{g : Map S′ Y Z}
→ π Z ∘ F.₁ (Push.₁ (map g 𝒞.∘ map f)) ∘ forget X 𝒟.≈ (π Z ∘ F.₁ (Push.₁ (map g)) ∘ forget Y) ∘ π Y ∘ F.₁ (Push.₁ (map f)) ∘ forget X
homo {X} {Y} {Z} {f′} {g′} = begin
π Z ∘ F.₁ (Push.₁ (g 𝒞.∘ f)) ∘ forget X ≈⟨ refl⟩∘⟨ F.F-resp-≈ Push.homomorphism ⟩∘⟨refl ⟩
π Z ∘ F.₁ (Push.₁ g BWD.∘ Push.₁ f) ∘ forget X ≈⟨ refl⟩∘⟨ pushˡ F.homomorphism ⟩
π Z ∘ F.₁ (Push.₁ g) ∘ F.₁ (Push.₁ f) ∘ forget X ≈⟨ pushˡ (𝒟.Equiv.sym (π∘l Z)) ⟩
π Z ∘ L Z ∘ F.₁ (Push.₁ g) ∘ F.₁ (Push.₁ f) ∘ forget X ≈⟨ refl⟩∘⟨ pullˡ (𝒟.Equiv.sym F.homomorphism) ⟩
π Z ∘ F.₁ (loop BWD.∘ Push.₁ g) ∘ F.₁ (Push.₁ f) ∘ forget X ≈⟨ refl⟩∘⟨ F.F-resp-≈ (loop∘push∘loop g (entire g′)) ⟩∘⟨refl ⟨
π Z ∘ F.₁ (loop BWD.∘ Push.₁ g BWD.∘ loop) ∘ F.₁ (Push.₁ f) ∘ forget X ≈⟨ refl⟩∘⟨ pushˡ F.homomorphism ⟩
π Z ∘ L Z ∘ F.₁ (Push.₁ g BWD.∘ loop) ∘ F.₁ (Push.₁ f) ∘ forget X ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ F.homomorphism ⟩
π Z ∘ L Z ∘ F.₁ (Push.₁ g) ∘ L Y ∘ F.₁ (Push.₁ f) ∘ forget X ≈⟨ pullˡ (π∘l Z) ⟩
π Z ∘ F.₁ (Push.₁ g) ∘ L Y ∘ F.₁ (Push.₁ f) ∘ forget X ≈⟨ pushʳ (pushʳ (pushˡ (𝒟.Equiv.sym (forget∘π Y)))) ⟩
(π Z ∘ F.₁ (Push.₁ g) ∘ forget Y) ∘ π Y ∘ F.₁ (Push.₁ f) ∘ forget X ∎
where
f : X 𝒞.⇒ Y
f = map f′
g : Y 𝒞.⇒ Z
g = map g′
resp : {A B : 𝒞.Obj} {f g : A 𝒞.⇒ B} → f 𝒞.≈ g → π B ∘ F.₁ (Push.₁ f) ∘ forget A 𝒟.≈ π B ∘ F.₁ (Push.₁ g) ∘ forget A
resp {A} {B} {f} {g} f≈g = refl⟩∘⟨ F.F-resp-≈ (Push.F-resp-≈ f≈g) ⟩∘⟨refl
|
