Mercurial > hg > Members > kono > Proof > category
annotate comparison-em.agda @ 122:f8fbd5ecec97
no yellow on em-category
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Fri, 02 Aug 2013 08:21:32 +0900 |
parents | 324511654f23 |
children | 44c58c27d12d |
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 |
121
324511654f23
add Comparison functor for EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
99
diff
changeset
|
36 M : Monad A (U^K ○ F^K ) η^K μ^K |
324511654f23
add Comparison functor for EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
99
diff
changeset
|
37 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
|
38 |
122
f8fbd5ecec97
no yellow on em-category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
121
diff
changeset
|
39 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
|
40 |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
41 open Functor |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
42 open NTrans |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
43 open Adjunction |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
44 open MResolution |
122
f8fbd5ecec97
no yellow on em-category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
121
diff
changeset
|
45 open Eilenberg-Moore-Hom |
98
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
46 |
121
324511654f23
add Comparison functor for EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
99
diff
changeset
|
47 emkobj : Obj B -> EMObj |
324511654f23
add Comparison functor for EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
99
diff
changeset
|
48 emkobj b = record { |
324511654f23
add Comparison functor for EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
99
diff
changeset
|
49 a = FObj U^K b ; phi = A [ FMap U^K o TMap ε^K b ] ; isAlgebra = record { identity = identity1; eval = eval1 } |
324511654f23
add Comparison functor for EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
99
diff
changeset
|
50 } where |
324511654f23
add Comparison functor for EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
99
diff
changeset
|
51 identity1 : ? |
324511654f23
add Comparison functor for EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
99
diff
changeset
|
52 identity1 = ? |
324511654f23
add Comparison functor for EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
99
diff
changeset
|
53 eval1 : ? |
324511654f23
add Comparison functor for EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
99
diff
changeset
|
54 eval1 = ? |
98
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
55 |
121
324511654f23
add Comparison functor for EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
99
diff
changeset
|
56 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
|
57 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
|
58 } where |
324511654f23
add Comparison functor for EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
99
diff
changeset
|
59 homomorphism1 : ? |
324511654f23
add Comparison functor for EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
99
diff
changeset
|
60 homomorphism1 = ? |
324511654f23
add Comparison functor for EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
99
diff
changeset
|
61 |
324511654f23
add Comparison functor for EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
99
diff
changeset
|
62 K^T : Functor B Eilenberg-MooreCategory |
324511654f23
add Comparison functor for EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
99
diff
changeset
|
63 K^T = record { |
324511654f23
add Comparison functor for EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
99
diff
changeset
|
64 FObj = emkobj |
324511654f23
add Comparison functor for EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
99
diff
changeset
|
65 ; FMap = emkmap |
98
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
66 ; isFunctor = record |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
67 { ≈-cong = ≈-cong |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
68 ; identity = identity |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
69 ; distr = distr1 |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
70 } |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
71 } where |
122
f8fbd5ecec97
no yellow on em-category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
121
diff
changeset
|
72 identity : {a : Obj A} → B [ emkmap (EM-id {a}) ≈ id1 B (FObj F^K a) ] |
98
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
73 identity {a} = let open ≈-Reasoning (B) in |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
74 begin |
122
f8fbd5ecec97
no yellow on em-category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
121
diff
changeset
|
75 emkmap (EM-id {a}) |
121
324511654f23
add Comparison functor for EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
99
diff
changeset
|
76 ≈⟨ ? ⟩ |
324511654f23
add Comparison functor for EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
99
diff
changeset
|
77 id1 B (FObj F^K a) |
98
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
78 ∎ |
122
f8fbd5ecec97
no yellow on em-category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
121
diff
changeset
|
79 ≈-cong : {a b : Obj A} -> {f g : EMHom a b} → A [ EMap f ≈ EMap g ] → B [ emkmap f ≈ emkmap g ] |
98
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
80 ≈-cong {a} {b} {f} {g} f≈g = let open ≈-Reasoning (B) in |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
81 begin |
121
324511654f23
add Comparison functor for EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
99
diff
changeset
|
82 emkmap f |
324511654f23
add Comparison functor for EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
99
diff
changeset
|
83 ≈⟨ ? ⟩ |
324511654f23
add Comparison functor for EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
99
diff
changeset
|
84 emkmap g |
98
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
85 ∎ |
122
f8fbd5ecec97
no yellow on em-category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
121
diff
changeset
|
86 distr1 : {a b c : Obj A} {f : EMHom a b} {g : EMHom b c} → B [ emkmap (g ∙ f) ≈ (B [ emkmap g o emkmap f ] )] |
98
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
87 distr1 {a} {b} {c} {f} {g} = let open ≈-Reasoning (B) in |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
88 begin |
122
f8fbd5ecec97
no yellow on em-category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
121
diff
changeset
|
89 emkmap (g ∙ f) |
121
324511654f23
add Comparison functor for EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
99
diff
changeset
|
90 ≈⟨ ? ⟩ |
324511654f23
add Comparison functor for EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
99
diff
changeset
|
91 emkmap g o emkmap f |
98
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
92 ∎ |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
93 |