Mercurial > hg > Members > kono > Proof > category
annotate comparison-em.agda @ 123:44c58c27d12d
problems written Comparison Functor on EM
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Fri, 02 Aug 2013 08:36:44 +0900 |
parents | f8fbd5ecec97 |
children | aaeb92b58647 |
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 { |
123
44c58c27d12d
problems written Comparison Functor on EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
122
diff
changeset
|
52 a = FObj U^K b ; phi = FMap U^K (TMap ε^K b) ; isAlgebra = record { identity = identity1; eval = eval1 } |
121
324511654f23
add Comparison functor for EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
99
diff
changeset
|
53 } where |
324511654f23
add Comparison functor for EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
99
diff
changeset
|
54 identity1 : ? |
324511654f23
add Comparison functor for EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
99
diff
changeset
|
55 identity1 = ? |
324511654f23
add Comparison functor for EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
99
diff
changeset
|
56 eval1 : ? |
324511654f23
add Comparison functor for EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
99
diff
changeset
|
57 eval1 = ? |
98
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
58 |
121
324511654f23
add Comparison functor for EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
99
diff
changeset
|
59 emkmap : {a b : Obj B} (f : Hom B a b) -> EMHom (emkobj a) (emkobj b) |
122
f8fbd5ecec97
no yellow on em-category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
121
diff
changeset
|
60 emkmap {a} {b} f = record { EMap = FMap U^K f ; homomorphism = homomorphism1 |
121
324511654f23
add Comparison functor for EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
99
diff
changeset
|
61 } where |
324511654f23
add Comparison functor for EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
99
diff
changeset
|
62 homomorphism1 : ? |
324511654f23
add Comparison functor for EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
99
diff
changeset
|
63 homomorphism1 = ? |
324511654f23
add Comparison functor for EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
99
diff
changeset
|
64 |
324511654f23
add Comparison functor for EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
99
diff
changeset
|
65 K^T : Functor B Eilenberg-MooreCategory |
324511654f23
add Comparison functor for EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
99
diff
changeset
|
66 K^T = record { |
324511654f23
add Comparison functor for EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
99
diff
changeset
|
67 FObj = emkobj |
324511654f23
add Comparison functor for EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
99
diff
changeset
|
68 ; FMap = emkmap |
98
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
69 ; isFunctor = record |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
70 { ≈-cong = ≈-cong |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
71 ; identity = identity |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
72 ; distr = distr1 |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
73 } |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
74 } where |
123
44c58c27d12d
problems written Comparison Functor on EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
122
diff
changeset
|
75 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
|
76 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
|
77 begin |
123
44c58c27d12d
problems written Comparison Functor on EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
122
diff
changeset
|
78 EMap (emkmap (id1 B a)) |
121
324511654f23
add Comparison functor for EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
99
diff
changeset
|
79 ≈⟨ ? ⟩ |
123
44c58c27d12d
problems written Comparison Functor on EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
122
diff
changeset
|
80 EMap (EM-id {emkobj a}) |
98
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
81 ∎ |
123
44c58c27d12d
problems written Comparison Functor on EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
122
diff
changeset
|
82 ≈-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
|
83 ≈-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
|
84 begin |
123
44c58c27d12d
problems written Comparison Functor on EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
122
diff
changeset
|
85 EMap (emkmap f) |
121
324511654f23
add Comparison functor for EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
99
diff
changeset
|
86 ≈⟨ ? ⟩ |
123
44c58c27d12d
problems written Comparison Functor on EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
122
diff
changeset
|
87 EMap (emkmap g) |
98
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
88 ∎ |
123
44c58c27d12d
problems written Comparison Functor on EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
122
diff
changeset
|
89 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
|
90 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
|
91 begin |
123
44c58c27d12d
problems written Comparison Functor on EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
122
diff
changeset
|
92 EMap (emkmap (B [ g o f ] )) |
121
324511654f23
add Comparison functor for EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
99
diff
changeset
|
93 ≈⟨ ? ⟩ |
123
44c58c27d12d
problems written Comparison Functor on EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
122
diff
changeset
|
94 EMap (emkmap g ∙ emkmap f) |
98
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
95 ∎ |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
96 |