Mercurial > hg > Members > kono > Proof > category

comparison src/comparison-functor.agda @ 949:ac53803b3b2a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
reorganization for apkg
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 21 Dec 2020 16:40:15 +0900
parents comparison-functor.agda@a5f2ca67e7c5
children 45de2b31bf02
comparison
equal deleted inserted replaced
948:dca4b29553cb 949:ac53803b3b2a
1 -- -- -- -- -- -- -- --
2 -- Comparison Functor of Kelisli Category
3 -- defines U_K and F_K as a resolution of Monad
4 -- checks Adjointness
5 --
6 -- Shinji KONO <kono@ie.u-ryukyu.ac.jp>
7 -- -- -- -- -- -- -- --
8
9 open import Category -- https://github.com/konn/category-agda
10 open import Level
11 --open import Category.HomReasoning
12 open import HomReasoning
13 open import cat-utility
14 open import Category.Cat
15 open import Relation.Binary.Core
16
17 module comparison-functor
18 { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ }
19 { T : Functor A A }
20 { η : NTrans A A identityFunctor T }
21 { μ : NTrans A A (T ○ T) T }
22 { M' : IsMonad A T η μ }
23 {c₁' c₂' ℓ' : Level} ( B : Category c₁' c₂' ℓ' )
24 { U_K : Functor B A } { F_K : Functor A B }
25 { η_K : NTrans A A identityFunctor ( U_K ○ F_K ) }
26 { ε_K : NTrans B B ( F_K ○ U_K ) identityFunctor }
27 { μ_K' : NTrans A A (( U_K ○ F_K ) ○ ( U_K ○ F_K )) ( U_K ○ F_K ) }
28 ( AdjK : IsAdjunction A B U_K F_K η_K ε_K )
29 where
30
31 open import adj-monad
32
33 T_K = U_K ○ F_K
34
35 μ_K : NTrans A A (( U_K ○ F_K ) ○ ( U_K ○ F_K )) ( U_K ○ F_K )
36 μ_K = UεF A B U_K F_K ε_K
37
38 M : IsMonad A (U_K ○ F_K ) η_K μ_K
39 M = Monad.isMonad ( Adj2Monad A B ( record { U = U_K; F = F_K ; η = η_K ; ε = ε_K ; isAdjunction = AdjK } ) )
40
41 open import kleisli {c₁} {c₂} {ℓ} {A} { U_K ○ F_K } { η_K } { μ_K } { M }
42
43 open Functor
44 open NTrans
45 open KleisliHom
46 open Adjunction
47 open MResolution
48
49 kfmap : {a b : Obj A} (f : KHom a b) → Hom B (FObj F_K a) (FObj F_K b)
50 kfmap {_} {b} f = B [ TMap ε_K (FObj F_K b) o FMap F_K (KMap f) ]
51
52 K_T : Functor KleisliCategory B
53 K_T = record {
54 FObj = FObj F_K
55 ; FMap = kfmap
56 ; isFunctor = record
57 { ≈-cong = ≈-cong
58 ; identity = identity
59 ; distr = distr1
60 }
61 } where
62 identity : {a : Obj A} → B [ kfmap (K-id {a}) ≈ id1 B (FObj F_K a) ]
63 identity {a} = let open ≈-Reasoning (B) in
64 begin
65 kfmap (K-id {a})
66 ≈⟨⟩
67 TMap ε_K (FObj F_K a) o FMap F_K (KMap (K-id {a}))
68 ≈⟨⟩
69 TMap ε_K (FObj F_K a) o FMap F_K (TMap η_K a)
70 ≈⟨ IsAdjunction.adjoint2 AdjK ⟩
71 id1 B (FObj F_K a)
72 ∎
73 ≈-cong : {a b : Obj A} → {f g : KHom a b} → A [ KMap f ≈ KMap g ] → B [ kfmap f ≈ kfmap g ]
74 ≈-cong {a} {b} {f} {g} f≈g = let open ≈-Reasoning (B) in
75 begin
76 kfmap f
77 ≈⟨⟩
78 TMap ε_K (FObj F_K b) o FMap F_K (KMap f)
79 ≈⟨ cdr ( fcong F_K f≈g) ⟩
80 TMap ε_K (FObj F_K b) o FMap F_K (KMap g)
81 ≈⟨⟩
82 kfmap g
83 ∎
84 distr1 : {a b c : Obj A} {f : KHom a b} {g : KHom b c} → B [ kfmap (g * f) ≈ (B [ kfmap g o kfmap f ] )]
85 distr1 {a} {b} {c} {f} {g} = let open ≈-Reasoning (B) in
86 begin
87 kfmap (g * f)
88 ≈⟨⟩
89 TMap ε_K (FObj F_K c) o FMap F_K (KMap (g * f))
90 ≈⟨⟩
91 TMap ε_K (FObj F_K c) o FMap F_K (A [ TMap μ_K c o A [ FMap ( U_K ○ F_K ) (KMap g) o KMap f ] ] )
92 ≈⟨ cdr ( distr F_K ) ⟩
93 TMap ε_K (FObj F_K c) o ( FMap F_K (TMap μ_K c) o ( FMap F_K (A [ FMap ( U_K ○ F_K ) (KMap g) o KMap f ])))
94 ≈⟨ cdr (cdr ( distr F_K )) ⟩
95 TMap ε_K (FObj F_K c) o ( FMap F_K (TMap μ_K c) o (( FMap F_K (FMap ( U_K ○ F_K ) (KMap g))) o (FMap F_K (KMap f))))
96 ≈⟨ cdr assoc ⟩
97 TMap ε_K (FObj F_K c) o ((( FMap F_K (TMap μ_K c) o ( FMap F_K (FMap (U_K ○ F_K) (KMap g))))) o (FMap F_K (KMap f)))
98 ≈⟨⟩
99 TMap ε_K (FObj F_K c) o (( FMap F_K ( FMap U_K ( TMap ε_K ( FObj F_K c ) )) o
100 ( FMap F_K (FMap (U_K ○ F_K) (KMap g)))) o (FMap F_K (KMap f)))
101 ≈⟨ sym (cdr assoc) ⟩
102 TMap ε_K (FObj F_K c) o (( FMap F_K ( FMap U_K ( TMap ε_K ( FObj F_K c ) ))) o
103 (( FMap F_K (FMap (U_K ○ F_K) (KMap g))) o (FMap F_K (KMap f))))
104 ≈⟨ assoc ⟩
105 (TMap ε_K (FObj F_K c) o ( FMap F_K ( FMap U_K ( TMap ε_K ( FObj F_K c ) )))) o
106 (( FMap F_K (FMap (U_K ○ F_K) (KMap g))) o (FMap F_K (KMap f)))
107 ≈⟨ car (sym (nat ε_K)) ⟩
108 (TMap ε_K (FObj F_K c) o ( TMap ε_K (FObj (F_K ○ U_K) (FObj F_K c)))) o
109 (( FMap F_K (FMap (U_K ○ F_K) (KMap g))) o (FMap F_K (KMap f)))
110 ≈⟨ sym assoc ⟩
111 TMap ε_K (FObj F_K c) o (( TMap ε_K (FObj (F_K ○ U_K) (FObj F_K c))) o
112 ((( FMap F_K (FMap (U_K ○ F_K) (KMap g)))) o (FMap F_K (KMap f))))
113 ≈⟨ cdr assoc ⟩
114 TMap ε_K (FObj F_K c) o ((( TMap ε_K (FObj (F_K ○ U_K) (FObj F_K c))) o
115 (( FMap F_K (FMap (U_K ○ F_K) (KMap g))))) o (FMap F_K (KMap f)))
116 ≈⟨ cdr ( car (
117 begin
118 TMap ε_K (FObj (F_K ○ U_K) (FObj F_K c)) o ((FMap F_K (FMap (U_K ○ F_K) (KMap g))))
119 ≈⟨⟩
120 TMap ε_K (FObj (F_K ○ U_K) (FObj F_K c)) o (FMap (F_K ○ U_K) (FMap F_K (KMap g)))
121 ≈⟨ sym (nat ε_K) ⟩
122 ( FMap F_K (KMap g)) o (TMap ε_K (FObj F_K b))
123 ∎
124 )) ⟩
125 TMap ε_K (FObj F_K c) o ((( FMap F_K (KMap g)) o (TMap ε_K (FObj F_K b))) o FMap F_K (KMap f))
126 ≈⟨ cdr (sym assoc) ⟩
127 TMap ε_K (FObj F_K c) o (( FMap F_K (KMap g)) o (TMap ε_K (FObj F_K b) o FMap F_K (KMap f)))
128 ≈⟨ assoc ⟩
129 (TMap ε_K (FObj F_K c) o FMap F_K (KMap g)) o (TMap ε_K (FObj F_K b) o FMap F_K (KMap f))
130 ≈⟨⟩
131 kfmap g o kfmap f
132 ∎
133
134 Lemma-K1 : {a b : Obj A} ( f : Hom A a b ) → B [ FMap K_T ( FMap F_T f) ≈ FMap F_K f ]
135 Lemma-K1 {a} {b} f = let open ≈-Reasoning (B) in
136 begin
137 FMap K_T ( FMap F_T f)
138 ≈⟨⟩
139 TMap ε_K (FObj F_K b) o FMap F_K (KMap( FMap F_T f))
140 ≈⟨⟩
141 TMap ε_K (FObj F_K b) o FMap F_K (A [ TMap η_K b o f ])
142 ≈⟨ cdr ( distr F_K) ⟩
143 TMap ε_K (FObj F_K b) o (FMap F_K (TMap η_K b) o FMap F_K f )
144 ≈⟨ assoc ⟩
145 (TMap ε_K (FObj F_K b) o FMap F_K (TMap η_K b)) o FMap F_K f
146 ≈⟨ car ( IsAdjunction.adjoint2 AdjK) ⟩
147 id1 B (FObj F_K b) o FMap F_K f
148 ≈⟨ idL ⟩
149 FMap F_K f
150 ∎
151
152 Lemma-K2 : {a b : Obj A} ( f : KHom a b ) → A [ FMap U_K ( FMap K_T f) ≈ FMap U_T f ]
153 Lemma-K2 {a} {b} f = let open ≈-Reasoning (A) in
154 begin
155 FMap U_K ( FMap K_T f)
156 ≈⟨⟩
157 FMap U_K ( B [ TMap ε_K (FObj F_K b) o FMap F_K (KMap f) ] )
158 ≈⟨ distr U_K ⟩
159 FMap U_K ( TMap ε_K (FObj F_K b)) o FMap U_K (FMap F_K (KMap f) )
160 ≈⟨⟩
161 TMap μ_K b o FMap T_K (KMap f)
162 ≈⟨⟩ -- the definition
163 FMap U_T f
164 ∎
165
166 Lemma-K3 : (b : Obj A) → B [ FMap K_T (record { KMap = (TMap η_K b) }) ≈ id1 B (FObj F_K b) ]
167 Lemma-K3 b = let open ≈-Reasoning (B) in
168 begin
169 FMap K_T (record { KMap = (TMap η_K b) })
170 ≈⟨⟩
171 TMap ε_K (FObj F_K b) o FMap F_K (TMap η_K b)
172 ≈⟨ IsAdjunction.adjoint2 AdjK ⟩
173 id1 B (FObj F_K b)
174 ∎
175
176 Lemma-K4 : (b c : Obj A) (g : Hom A b (FObj T_K c)) →
177 B [ FMap K_T ( record { KMap = A [ (TMap η_K (FObj T_K c)) o g ] }) ≈ FMap F_K g ]
178 Lemma-K4 b c g = let open ≈-Reasoning (B) in
179 begin
180 FMap K_T ( record { KMap = A [ (TMap η_K (FObj T_K c)) o g ] })
181 ≈⟨⟩
182 TMap ε_K (FObj F_K (FObj T_K c)) o FMap F_K (A [ (TMap η_K (FObj T_K c)) o g ])
183 ≈⟨ cdr (distr F_K) ⟩
184 TMap ε_K (FObj F_K (FObj T_K c)) o ( FMap F_K (TMap η_K (FObj T_K c)) o FMap F_K g )
185 ≈⟨ assoc ⟩
186 (TMap ε_K (FObj F_K (FObj T_K c)) o ( FMap F_K (TMap η_K (FObj T_K c)))) o FMap F_K g
187 ≈⟨ car ( IsAdjunction.adjoint2 AdjK) ⟩
188 id1 B (FObj F_K (FObj T_K c)) o FMap F_K g
189 ≈⟨ idL ⟩
190 FMap F_K g
191 ∎
192
193 -- Lemma-K5 : (a : Obj A) → FObj U_K ( FObj K_T a ) = U_T a
194
195 Lemma-K6 : (b c : Obj A) (g : KHom b c) → A [ FMap U_K ( FMap K_T g ) ≈ FMap U_T g ]
196 Lemma-K6 b c g = let open ≈-Reasoning (A) in
197 begin
198 FMap U_K ( FMap K_T g )
199 ≈⟨⟩
200 FMap U_K ( B [ TMap ε_K ( FObj F_K c ) o FMap F_K (KMap g) ] )
201 ≈⟨ distr U_K ⟩
202 FMap U_K ( TMap ε_K ( FObj F_K c )) o FMap U_K ( FMap F_K (KMap g) )
203 ≈⟨⟩
204 TMap μ_K c o FMap U_K ( FMap F_K (KMap g) )
205 ≈⟨⟩
206 FMap U_T g
207 ∎
208
209