Mercurial > hg > Members > kono > Proof > category
annotate comparison-em.agda @ 124:aaeb92b58647
on going
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Fri, 02 Aug 2013 08:50:22 +0900 |
parents | 44c58c27d12d |
children | dec1f5db1edd |
rev | line source |
---|---|
98
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
1 -- -- -- -- -- -- -- -- |
121
324511654f23
add Comparison functor for EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
99
diff
changeset
|
2 -- Comparison Functor of Eilenberg-Moore Category |
324511654f23
add Comparison functor for EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
99
diff
changeset
|
3 -- defines U^K and F^K as a resolution of Monad |
98
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
4 -- checks Adjointness |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
5 -- |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
6 -- Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
7 -- -- -- -- -- -- -- -- |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
8 |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
9 open import Category -- https://github.com/konn/category-agda |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
10 open import Level |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
11 --open import Category.HomReasoning |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
12 open import HomReasoning |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
13 open import cat-utility |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
14 open import Category.Cat |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
15 open import Relation.Binary.Core |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
16 |
121
324511654f23
add Comparison functor for EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
99
diff
changeset
|
17 module comparison-em |
98
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
18 { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
19 { T : Functor A A } |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
20 { η : NTrans A A identityFunctor T } |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
21 { μ : NTrans A A (T ○ T) T } |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
22 { M' : Monad A T η μ } |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
23 {c₁' c₂' ℓ' : Level} ( B : Category c₁' c₂' ℓ' ) |
121
324511654f23
add Comparison functor for EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
99
diff
changeset
|
24 { U^K : Functor B A } { F^K : Functor A B } |
324511654f23
add Comparison functor for EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
99
diff
changeset
|
25 { η^K : NTrans A A identityFunctor ( U^K ○ F^K ) } |
324511654f23
add Comparison functor for EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
99
diff
changeset
|
26 { ε^K : NTrans B B ( F^K ○ U^K ) identityFunctor } |
122
f8fbd5ecec97
no yellow on em-category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
121
diff
changeset
|
27 { μ^K : NTrans A A (( U^K ○ F^K ) ○ ( U^K ○ F^K )) ( U^K ○ F^K ) } |
121
324511654f23
add Comparison functor for EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
99
diff
changeset
|
28 ( Adj^K : Adjunction A B U^K F^K η^K ε^K ) |
122
f8fbd5ecec97
no yellow on em-category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
121
diff
changeset
|
29 ( RK : MResolution A B T U^K F^K {η^K} {ε^K} {μ^K} Adj^K ) |
98
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
30 where |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
31 |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
32 open import adj-monad |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
33 |
121
324511654f23
add Comparison functor for EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
99
diff
changeset
|
34 T^K = U^K ○ F^K |
98
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
35 |
123
44c58c27d12d
problems written Comparison Functor on EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
122
diff
changeset
|
36 μ^K' : NTrans A A (( U^K ○ F^K ) ○ ( U^K ○ F^K )) ( U^K ○ F^K ) |
44c58c27d12d
problems written Comparison Functor on EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
122
diff
changeset
|
37 μ^K' = UεF A B U^K F^K ε^K |
44c58c27d12d
problems written Comparison Functor on EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
122
diff
changeset
|
38 |
44c58c27d12d
problems written Comparison Functor on EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
122
diff
changeset
|
39 M : Monad A (U^K ○ F^K ) η^K μ^K' |
121
324511654f23
add Comparison functor for EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
99
diff
changeset
|
40 M = Adj2Monad A B {U^K} {F^K} {η^K} {ε^K} Adj^K |
98
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
41 |
123
44c58c27d12d
problems written Comparison Functor on EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
122
diff
changeset
|
42 open import em-category {c₁} {c₂} {ℓ} {A} { U^K ○ F^K } { η^K } { μ^K' } { M } |
98
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
43 |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
44 open Functor |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
45 open NTrans |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
46 open Adjunction |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
47 open MResolution |
122
f8fbd5ecec97
no yellow on em-category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
121
diff
changeset
|
48 open Eilenberg-Moore-Hom |
98
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
49 |
121
324511654f23
add Comparison functor for EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
99
diff
changeset
|
50 emkobj : Obj B -> EMObj |
324511654f23
add Comparison functor for EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
99
diff
changeset
|
51 emkobj b = record { |
124 | 52 a = FObj U^K b ; phi = FMap U^K (TMap ε^K b) ; isAlgebra = record { identity = identity1 b; eval = eval1 b } |
121
324511654f23
add Comparison functor for EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
99
diff
changeset
|
53 } where |
124 | 54 identity1 : (b : Obj B) -> A [ A [ (FMap U^K (TMap ε^K b)) o TMap η^K (FObj U^K b) ] ≈ id1 A (FObj U^K b) ] |
55 identity1 b = {!!} | |
56 eval1 : (b : Obj B) -> A [ A [ (FMap U^K (TMap ε^K b)) o TMap μ^K' (FObj U^K b) ] ≈ A [ (FMap U^K (TMap ε^K b)) o FMap T^K (FMap U^K (TMap ε^K b)) ] ] | |
57 eval1 b = {!!} | |
98
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
58 |
124 | 59 open EMObj |
121
324511654f23
add Comparison functor for EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
99
diff
changeset
|
60 emkmap : {a b : Obj B} (f : Hom B a b) -> EMHom (emkobj a) (emkobj b) |
124 | 61 emkmap {a} {b} f = record { EMap = FMap U^K f ; homomorphism = homomorphism1 a b f |
121
324511654f23
add Comparison functor for EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
99
diff
changeset
|
62 } where |
124 | 63 homomorphism1 : (a b : Obj B) (f : Hom B a b) -> A [ A [ (φ (emkobj b)) o FMap T^K (FMap U^K f) ] ≈ A [ (FMap U^K f) o (φ (emkobj a)) ] ] |
64 homomorphism1 a b f = {!!} | |
121
324511654f23
add Comparison functor for EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
99
diff
changeset
|
65 |
324511654f23
add Comparison functor for EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
99
diff
changeset
|
66 K^T : Functor B Eilenberg-MooreCategory |
324511654f23
add Comparison functor for EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
99
diff
changeset
|
67 K^T = record { |
324511654f23
add Comparison functor for EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
99
diff
changeset
|
68 FObj = emkobj |
324511654f23
add Comparison functor for EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
99
diff
changeset
|
69 ; FMap = emkmap |
98
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
70 ; isFunctor = record |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
71 { ≈-cong = ≈-cong |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
72 ; identity = identity |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
73 ; distr = distr1 |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
74 } |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
75 } where |
123
44c58c27d12d
problems written Comparison Functor on EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
122
diff
changeset
|
76 identity : {a : Obj B} → emkmap (id1 B a) ≗ EM-id {emkobj a} |
44c58c27d12d
problems written Comparison Functor on EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
122
diff
changeset
|
77 identity {a} = let open ≈-Reasoning (A) in |
98
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
78 begin |
123
44c58c27d12d
problems written Comparison Functor on EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
122
diff
changeset
|
79 EMap (emkmap (id1 B a)) |
124 | 80 ≈⟨ {!!} ⟩ |
123
44c58c27d12d
problems written Comparison Functor on EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
122
diff
changeset
|
81 EMap (EM-id {emkobj a}) |
98
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
82 ∎ |
123
44c58c27d12d
problems written Comparison Functor on EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
122
diff
changeset
|
83 ≈-cong : {a b : Obj B} -> {f g : Hom B a b} → B [ f ≈ g ] → emkmap f ≗ emkmap g |
44c58c27d12d
problems written Comparison Functor on EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
122
diff
changeset
|
84 ≈-cong {a} {b} {f} {g} f≈g = let open ≈-Reasoning (A) in |
98
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
85 begin |
123
44c58c27d12d
problems written Comparison Functor on EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
122
diff
changeset
|
86 EMap (emkmap f) |
124 | 87 ≈⟨ {!!} ⟩ |
123
44c58c27d12d
problems written Comparison Functor on EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
122
diff
changeset
|
88 EMap (emkmap g) |
98
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
89 ∎ |
123
44c58c27d12d
problems written Comparison Functor on EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
122
diff
changeset
|
90 distr1 : {a b c : Obj B} {f : Hom B a b} {g : Hom B b c} → ( (emkmap (B [ g o f ])) ≗ (emkmap g ∙ emkmap f) ) |
44c58c27d12d
problems written Comparison Functor on EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
122
diff
changeset
|
91 distr1 {a} {b} {c} {f} {g} = let open ≈-Reasoning (A) in |
98
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
92 begin |
123
44c58c27d12d
problems written Comparison Functor on EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
122
diff
changeset
|
93 EMap (emkmap (B [ g o f ] )) |
124 | 94 ≈⟨ {!!} ⟩ |
123
44c58c27d12d
problems written Comparison Functor on EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
122
diff
changeset
|
95 EMap (emkmap g ∙ emkmap f) |
98
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
96 ∎ |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
97 |