-
Notifications
You must be signed in to change notification settings - Fork 1
/
ComonadMorph2DContainerMorph.agda
163 lines (147 loc) · 9.18 KB
/
ComonadMorph2DContainerMorph.agda
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
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
{-# OPTIONS --type-in-type #-}
open import Utils
open import Containers
open import DContainers renaming (_∘_ to _∘'_ ; ⇒-id to ⇒-id' ; ⌈_⌉ to ⌈_⌉' ; _⇒_ to _⇒'_)
open import DContainerExt renaming (⟦_⟧₀ to ⟦_⟧₀' ; ⟦_⟧₁ to ⟦_⟧₁')
open import Comonads renaming (_c∘_ to _c∘'_)
open import Functors
open import Comonad2DContainer
open import Comonad2DContainerHelper
open import ComonadMorph2DContainerMorphHelper
module ComonadMorph2DContainerMorph where
open Container
open DContainer renaming (Shape to Shape' ; Pos to Pos')
open Containers._⇒_
open Functor
open Comonad
open _⇛_
open _⇨_
⌜_,_,_,_,_⌝ : (CM₀ CM₁ : Comonad) → {C₀ C₁ : Container} → (q₀ : Fun CM₀ == ⟦ C₀ ⟧₀) → (q₁ : Fun CM₁ == ⟦ C₁ ⟧₀) → CM₀ ⇨ CM₁ → ⌈ CM₀ , q₀ ⌉ ⇒' ⌈ CM₁ , q₁ ⌉
⌜_,_,_,_,_⌝ (CM .(Functor⋆ (λ X → ∃ (Shape C₀) (λ s → (Pos C₀) s → X)) (fmap'.fmap' (Shape C₀) (Pos C₀)) refl refl) counit₀ comult₀ lunit₀ runit₀ assoc₀) (CM .(Functor⋆ (λ X → ∃ (Shape C₁) (λ s → (Pos C₁) s → X)) (fmap'.fmap' (Shape C₁) (Pos C₁)) refl refl) counit₁ comult₁ lunit₁ runit₁ assoc₁) {C₀} {C₁} refl refl h = _◁_ sf' pf' ax6' ax7' ax8' where
C₀' : DContainer
C₀' = ⌈ (CM (Functor⋆ (λ X → ∃ (Shape C₀) (λ s → (Pos C₀) s → X)) (fmap'.fmap' (Shape C₀) (Pos C₀)) refl refl) counit₀ comult₀ lunit₀ runit₀ assoc₀) , refl ⌉
C₁' : DContainer
C₁' = ⌈ (CM (Functor⋆ (λ X → ∃ (Shape C₁) (λ s → (Pos C₁) s → X)) (fmap'.fmap' (Shape C₁) (Pos C₁)) refl refl) counit₁ comult₁ lunit₁ runit₁ assoc₁) , refl ⌉
counit₀' : C₀ ⇒ Id-Con
counit₀' = ⌜ NatIso.j e-iso ∘ counit₀ ⌝
comult₀' : C₀ ⇒ C₀ [ C₀ ]
comult₀' = ⌜ NatIso.j (m-iso C₀ C₀ ) ∘ comult₀ ⌝
counit₁' : C₁ ⇒ Id-Con
counit₁' = ⌜ NatIso.j e-iso ∘ counit₁ ⌝
comult₁' : C₁ ⇒ C₁ [ C₁ ]
comult₁' = ⌜ NatIso.j (m-iso C₁ C₁ ) ∘ comult₁ ⌝
abstract
comult₀'-ax1 : ∀ {s} → ∃.fst∃ (tr comult₀ (s , identity)) == s
comult₀'-ax1 {s} = cong' refl refl (cong sf (fully-faithful-lem3-c {_} {_} {(⌜ (⟦ C₀ ⟧₀ F∘ NatIso.i e-iso) ∘ NatIso.i (m-iso C₀ (Id-Con)) ⌝) ◦ (C₀ C◦ ⌜ NatIso.j e-iso ∘ counit₀ ⌝) ◦ ⌜ NatIso.j (m-iso C₀ C₀ ) ∘ comult₀ ⌝} {⇒-id {C₀}} (runit-lem {C₀} {counit₀} {comult₀} {runit₀})))
sf' : Shape C₀ → Shape C₁
sf' s = sf ⌜ tr' h ⌝ s
pf' : {s : Shape C₀} → Pos C₁ (sf' s) → Pos C₀ s
pf' {s} p = pf ⌜ tr' h ⌝ s p
abstract
ax6' : {s : Shape C₀} → {p : Pos' C₁' (sf' s)} → _↓_ C₁' (sf' s) p == sf' (_↓_ C₀' s (pf' {s} p))
ax6' {s} {p} = trans
(cong' {_} {_} {_}
{subst (λ x → Pos C₁ (∃.fst∃ (tr (tr' h) (x , identity)))) p (sym comult₀'-ax1)}
(trans
(stripsubst (Pos C₁) p (sym (c2dc.comult'-ax1 counit₁ comult₁ lunit₁ runit₁ assoc₁)))
(sym
(stripsubst (λ x → Pos C₁ (∃.fst∃ (tr (tr' h) (x , identity)))) p (sym comult₀'-ax1))))
(ext' (λ x → refl))
(∃-eqsnd refl refl
(cong' {_} {_} {s} {s} refl refl
(cong sf
(fully-faithful-lem3-c {_} {_}
{⌜ NatIso.j (m-iso C₁ C₁ ) ∘ comult₁ ⌝ ◦ ⌜ tr' h ⌝}
{(C₁ C◦ ⌜ tr' h ⌝) ◦ (⌜ tr' h ⌝ ◦C C₀) ◦ ⌜ NatIso.j (m-iso C₀ C₀ ) ∘ comult₀ ⌝}
(cm-lem {C₀} {C₁} {counit₀} {comult₀} {lunit₀} {runit₀} {assoc₀} {counit₁} {comult₁} {lunit₁} {runit₁} {assoc₁} {h}))))))
(cong
(λ x → ∃.fst∃ (tr (tr' h) (∃.fst∃ (∃.snd∃ (tr comult₀ (s , identity)) x) , identity)))
(trans
(cong2
(λ x y → ∃.snd∃ (tr (tr' h) (x , identity)) y)
comult₀'-ax1
(stripsubst (λ x → Pos C₁ (∃.fst∃ (tr (tr' h) (x , identity)))) p (sym comult₀'-ax1)))
(sym
(stripsubst (Pos C₀) (∃.snd∃ (tr (tr' h) (s , identity)) p) (sym (c2dc.comult'-ax1 counit₀ comult₀ lunit₀ runit₀ assoc₀))))))
ax7' : {s : Shape C₀} → pf' {s} (o C₁') == o C₀' {s}
ax7' {s} = cong' refl refl
(cong' refl refl
(cong pf
(fully-faithful-lem3-c {_} {_}
{⌜ NatIso.j e-iso ∘ counit₁ ⌝ ◦ ⌜ tr' h ⌝}
{⌜ NatIso.j e-iso ∘ counit₀ ⌝}
(cu-lem {C₀} {C₁} {counit₀} {comult₀} {lunit₀} {runit₀} {assoc₀} {counit₁} {comult₁} {lunit₁} {runit₁} {assoc₁} {h}))))
ax8' : {s : Shape C₀} → (p : Pos' C₁' (sf' s)) → (p' : Pos' C₁' (_↓_ C₁' (sf' s) p)) → pf' {s} (_⊕_ C₁' p p') == _⊕_ C₀' (pf' {s} p) (pf' (subst (Pos' C₁') p' ax6'))
ax8' {s} p p' = trans
(cong' {_} {_} {_}
{(subst (λ x → Pos C₁ (∃.fst∃ (tr (tr' h) (x , identity)))) p (sym comult₀'-ax1)) ,
(subst (Pos C₁) p' (trans (ax6' {s} {p})
(cong
(λ x → ∃.fst∃ (tr (tr' h) (∃.fst∃ (∃.snd∃ (tr comult₀ (s , identity)) x) , identity)))
(trans
(stripsubst (Pos C₀) (∃.snd∃ (tr (tr' h) (s , identity)) p) (sym (c2dc.comult'-ax1 counit₀ comult₀ lunit₀ runit₀ assoc₀)))
(cong2 (λ x y → ∃.snd∃ (tr (tr' h) (x , identity)) y) (sym comult₀'-ax1) (sym (stripsubst (λ x → Pos C₁ (∃.fst∃ (tr (tr' h) (x , identity)))) p (sym comult₀'-ax1))))))))}
(∃-eq
(ext' (λ {p0} {p1} q → cong (Pos C₁)
(trans
(cong2
(λ x y → ∃.fst∃ (∃.snd∃ (tr comult₁ (∃.fst∃ (tr (tr' h) (x , identity)) , identity)) y))
(sym comult₀'-ax1)
(trans q (sym (stripsubst (Pos C₁) p1 (sym (c2dc.comult'-ax1 counit₁ comult₁ lunit₁ runit₁ assoc₁))))))
(trans
(ax6' {∃.fst∃ (tr comult₀ (s , identity))} {p1})
(cong2
(λ x y → ∃.fst∃ (tr (tr' h) (∃.fst∃ (∃.snd∃ (tr comult₀ (x , identity)) y) , identity)))
comult₀'-ax1
(stripsubst (Pos C₀)
(∃.snd∃ (tr (tr' h) (∃.fst∃ (tr comult₀ (s , identity)) , identity)) p1)
(sym (c2dc.comult'-ax1 counit₀ comult₀ lunit₀ runit₀ assoc₀))))))))
(trans
(stripsubst (Pos C₁) p (sym (c2dc.comult'-ax1 counit₁ comult₁ lunit₁ runit₁ assoc₁)))
(sym (stripsubst (λ x → Pos C₁ (∃.fst∃ (tr (tr' h) (x , identity)))) p (sym comult₀'-ax1))))
(sym
(stripsubst (Pos C₁) p'
(trans
ax6'
(cong
(λ x → ∃.fst∃ (tr (tr' h) (∃.fst∃ (∃.snd∃ (tr comult₀ (s , identity)) x) , identity)))
(trans
(stripsubst (Pos C₀) (∃.snd∃ (tr (tr' h) (s , identity)) p) (sym (c2dc.comult'-ax1 counit₀ comult₀ lunit₀ runit₀ assoc₀)))
(cong2
(λ x y → ∃.snd∃ (tr (tr' h) (x , identity)) y)
(sym comult₀'-ax1)
(sym (stripsubst (λ x → Pos C₁ (∃.fst∃ (tr (tr' h) (x , identity)))) p (sym comult₀'-ax1))))))))))
(ext' (λ x → refl))
(cong2 pf
(fully-faithful-lem3-c {_} {_}
{⌜ NatIso.j (m-iso C₁ C₁ ) ∘ comult₁ ⌝ ◦ ⌜ tr' h ⌝}
{(C₁ C◦ ⌜ tr' h ⌝) ◦ (⌜ tr' h ⌝ ◦C C₀) ◦ ⌜ NatIso.j (m-iso C₀ C₀ ) ∘ comult₀ ⌝}
(cm-lem {C₀} {C₁} {counit₀} {comult₀} {lunit₀} {runit₀} {assoc₀} {counit₁} {comult₁} {lunit₁} {runit₁} {assoc₁} {h}))
refl))
(cong2
(λ x y → ∃.snd∃ (∃.snd∃ (tr comult₀ (s , identity)) x) y)
(trans
(cong2
(λ x y → ∃.snd∃ (tr (tr' h) (x , identity)) y)
comult₀'-ax1
(stripsubst (λ x → Pos C₁ (∃.fst∃ (tr (tr' h) (x , identity)))) p (sym comult₀'-ax1)))
(sym
(stripsubst (Pos C₀) (∃.snd∃ (tr (tr' h) (s , identity)) p) (sym (c2dc.comult'-ax1 counit₀ comult₀ lunit₀ runit₀ assoc₀)))))
(cong2
(λ x y → ∃.snd∃ (tr (tr' h) (∃.fst∃ (∃.snd∃ (tr comult₀ (s , identity)) x) , identity)) y)
(trans
(cong2 (λ y z → ∃.snd∃ (tr (tr' h) (y , identity)) z) comult₀'-ax1 (stripsubst (λ x → Pos C₁ (∃.fst∃ (tr (tr' h) (x , identity)))) p (sym comult₀'-ax1)))
(sym (stripsubst (Pos C₀) (∃.snd∃ (tr (tr' h) (s , identity)) p) (sym (c2dc.comult'-ax1 counit₀ comult₀ lunit₀ runit₀ assoc₀)))))
(trans
(stripsubst (Pos C₁) p'
(trans
ax6'
(cong
(λ x → ∃.fst∃ (tr (tr' h) (∃.fst∃ (∃.snd∃ (tr comult₀ (s , identity)) x) , identity)))
(trans
(stripsubst (Pos C₀) (∃.snd∃ (tr (tr' h) (s , identity)) p) (sym (c2dc.comult'-ax1 counit₀ comult₀ lunit₀ runit₀ assoc₀)))
(cong2
(λ x y → ∃.snd∃ (tr (tr' h) (x , identity)) y)
(sym comult₀'-ax1)
(sym (stripsubst (λ x → Pos C₁ (∃.fst∃ (tr (tr' h) (x , identity)))) p (sym comult₀'-ax1))))))))
(sym (stripsubst (Pos C₁) p' ax6')))))