Mercurial > hg > Members > kono > Proof > category

comparison comparison-functor.agda @ 688:a5f2ca67e7c5

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix monad/adjunction definition couniversal to limit does not work
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 11 Nov 2017 21:34:58 +0900
parents d3cd28a71b3f
children
comparison
equal deleted inserted replaced
687:d0bc017c6b61 688:a5f2ca67e7c5
17 module comparison-functor 17 module comparison-functor
18 { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } 18 { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ }
19 { T : Functor A A } 19 { T : Functor A A }
20 { η : NTrans A A identityFunctor T } 20 { η : NTrans A A identityFunctor T }
21 { μ : NTrans A A (T ○ T) T } 21 { μ : NTrans A A (T ○ T) T }
22 { M' : Monad A T η μ } 22 { M' : IsMonad A T η μ }
23 {c₁' c₂' ℓ' : Level} ( B : Category c₁' c₂' ℓ' ) 23 {c₁' c₂' ℓ' : Level} ( B : Category c₁' c₂' ℓ' )
24 { U_K : Functor B A } { F_K : Functor A B } 24 { U_K : Functor B A } { F_K : Functor A B }
25 { η_K : NTrans A A identityFunctor ( U_K ○ F_K ) } 25 { η_K : NTrans A A identityFunctor ( U_K ○ F_K ) }
26 { ε_K : NTrans B B ( F_K ○ U_K ) identityFunctor } 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 ) } 27 { μ_K' : NTrans A A (( U_K ○ F_K ) ○ ( U_K ○ F_K )) ( U_K ○ F_K ) }
28 ( AdjK : Adjunction A B U_K F_K η_K ε_K ) 28 ( AdjK : IsAdjunction A B U_K F_K η_K ε_K )
29 ( RK : MResolution A B T U_K F_K {η_K} {ε_K} {μ_K'} AdjK )
30 where 29 where
31 30
32 open import adj-monad 31 open import adj-monad
33 32
34 T_K = U_K ○ F_K 33 T_K = U_K ○ F_K
35 34
36 μ_K : NTrans A A (( U_K ○ F_K ) ○ ( U_K ○ F_K )) ( U_K ○ F_K ) 35 μ_K : NTrans A A (( U_K ○ F_K ) ○ ( U_K ○ F_K )) ( U_K ○ F_K )
37 μ_K = UεF A B U_K F_K ε_K 36 μ_K = UεF A B U_K F_K ε_K
38 37
39 M : Monad A (U_K ○ F_K ) η_K μ_K 38 M : IsMonad A (U_K ○ F_K ) η_K μ_K
40 M = Adj2Monad A B {U_K} {F_K} {η_K} {ε_K} AdjK 39 M = Monad.isMonad ( Adj2Monad A B ( record { U = U_K; F = F_K ; η = η_K ; ε = ε_K ; isAdjunction = AdjK } ) )
41 40
42 open import kleisli {c₁} {c₂} {ℓ} {A} { U_K ○ F_K } { η_K } { μ_K } { M } 41 open import kleisli {c₁} {c₂} {ℓ} {A} { U_K ○ F_K } { η_K } { μ_K } { M }
43 42
44 open Functor 43 open Functor
45 open NTrans 44 open NTrans
66 kfmap (K-id {a}) 65 kfmap (K-id {a})
67 ≈⟨⟩ 66 ≈⟨⟩
68 TMap ε_K (FObj F_K a) o FMap F_K (KMap (K-id {a})) 67 TMap ε_K (FObj F_K a) o FMap F_K (KMap (K-id {a}))
69 ≈⟨⟩ 68 ≈⟨⟩
70 TMap ε_K (FObj F_K a) o FMap F_K (TMap η_K a) 69 TMap ε_K (FObj F_K a) o FMap F_K (TMap η_K a)
71 ≈⟨ IsAdjunction.adjoint2 (isAdjunction AdjK) ⟩ 70 ≈⟨ IsAdjunction.adjoint2 AdjK ⟩
72 id1 B (FObj F_K a) 71 id1 B (FObj F_K a)
73 ∎ 72 ∎
74 ≈-cong : {a b : Obj A} → {f g : KHom a b} → A [ KMap f ≈ KMap g ] → B [ kfmap f ≈ kfmap g ] 73 ≈-cong : {a b : Obj A} → {f g : KHom a b} → A [ KMap f ≈ KMap g ] → B [ kfmap f ≈ kfmap g ]
75 ≈-cong {a} {b} {f} {g} f≈g = let open ≈-Reasoning (B) in 74 ≈-cong {a} {b} {f} {g} f≈g = let open ≈-Reasoning (B) in
76 begin 75 begin
142 TMap ε_K (FObj F_K b) o FMap F_K (A [ TMap η_K b o f ]) 141 TMap ε_K (FObj F_K b) o FMap F_K (A [ TMap η_K b o f ])
143 ≈⟨ cdr ( distr F_K) ⟩ 142 ≈⟨ cdr ( distr F_K) ⟩
144 TMap ε_K (FObj F_K b) o (FMap F_K (TMap η_K b) o FMap F_K f ) 143 TMap ε_K (FObj F_K b) o (FMap F_K (TMap η_K b) o FMap F_K f )
145 ≈⟨ assoc ⟩ 144 ≈⟨ assoc ⟩
146 (TMap ε_K (FObj F_K b) o FMap F_K (TMap η_K b)) o FMap F_K f 145 (TMap ε_K (FObj F_K b) o FMap F_K (TMap η_K b)) o FMap F_K f
147 ≈⟨ car ( IsAdjunction.adjoint2 (isAdjunction AdjK)) ⟩ 146 ≈⟨ car ( IsAdjunction.adjoint2 AdjK) ⟩
148 id1 B (FObj F_K b) o FMap F_K f 147 id1 B (FObj F_K b) o FMap F_K f
149 ≈⟨ idL ⟩ 148 ≈⟨ idL ⟩
150 FMap F_K f 149 FMap F_K f
151 ∎ 150 ∎
152 151
168 Lemma-K3 b = let open ≈-Reasoning (B) in 167 Lemma-K3 b = let open ≈-Reasoning (B) in
169 begin 168 begin
170 FMap K_T (record { KMap = (TMap η_K b) }) 169 FMap K_T (record { KMap = (TMap η_K b) })
171 ≈⟨⟩ 170 ≈⟨⟩
172 TMap ε_K (FObj F_K b) o FMap F_K (TMap η_K b) 171 TMap ε_K (FObj F_K b) o FMap F_K (TMap η_K b)
173 ≈⟨ IsAdjunction.adjoint2 (isAdjunction AdjK) ⟩ 172 ≈⟨ IsAdjunction.adjoint2 AdjK ⟩
174 id1 B (FObj F_K b) 173 id1 B (FObj F_K b)
175 ∎ 174 ∎
176 175
177 Lemma-K4 : (b c : Obj A) (g : Hom A b (FObj T_K c)) → 176 Lemma-K4 : (b c : Obj A) (g : Hom A b (FObj T_K c)) →
178 B [ FMap K_T ( record { KMap = A [ (TMap η_K (FObj T_K c)) o g ] }) ≈ FMap F_K g ] 177 B [ FMap K_T ( record { KMap = A [ (TMap η_K (FObj T_K c)) o g ] }) ≈ FMap F_K g ]
183 TMap ε_K (FObj F_K (FObj T_K c)) o FMap F_K (A [ (TMap η_K (FObj T_K c)) o g ]) 182 TMap ε_K (FObj F_K (FObj T_K c)) o FMap F_K (A [ (TMap η_K (FObj T_K c)) o g ])
184 ≈⟨ cdr (distr F_K) ⟩ 183 ≈⟨ cdr (distr F_K) ⟩
185 TMap ε_K (FObj F_K (FObj T_K c)) o ( FMap F_K (TMap η_K (FObj T_K c)) o FMap F_K g ) 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 )
186 ≈⟨ assoc ⟩ 185 ≈⟨ assoc ⟩
187 (TMap ε_K (FObj F_K (FObj T_K c)) o ( FMap F_K (TMap η_K (FObj T_K c)))) o FMap F_K g 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
188 ≈⟨ car ( IsAdjunction.adjoint2 (isAdjunction AdjK)) ⟩ 187 ≈⟨ car ( IsAdjunction.adjoint2 AdjK) ⟩
189 id1 B (FObj F_K (FObj T_K c)) o FMap F_K g 188 id1 B (FObj F_K (FObj T_K c)) o FMap F_K g
190 ≈⟨ idL ⟩ 189 ≈⟨ idL ⟩
191 FMap F_K g 190 FMap F_K g
192 ∎ 191 ∎
193 192