Mercurial > hg > Members > kono > Proof > category

annotate comparison-em.agda @ 121:324511654f23

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add Comparison functor for EM
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 01 Aug 2013 18:14:42 +0900
parents comparison-functor.agda@bd542a1caf08
children f8fbd5ecec97
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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 }
324511654f23 add Comparison functor for EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 99
diff changeset
27 { μ^K' : NTrans A A (( U^K ○ F^K ) ○ ( U^K ○ F^K )) ( U^K ○ F^K ) }
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 )
324511654f23 add Comparison functor for EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 99
diff changeset
29 ( RK : MResolution A B T U^K F^K {η^K} {ε^K} {μ^K'} AdjK )
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
121
324511654f23 add Comparison functor for EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 99
diff changeset
39 K : Eilenberg-MooreCategory 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 K = record {}
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
41
121
324511654f23 add Comparison functor for EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 99
diff changeset
42 open import nat {c₁} {c₂} {ℓ} {A} { U^K ○ F^K } { η^K } { μ^K } { M } { K }
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
121
324511654f23 add Comparison functor for EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 99
diff changeset
46 open Eilenberg-MooreCategory
324511654f23 add Comparison functor for EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 99
diff changeset
47 open EMHom
98
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
48 open Adjunction
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
49 open MResolution
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
50
121
324511654f23 add Comparison functor for EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 99
diff changeset
51 emkobj : Obj B -> EMObj
324511654f23 add Comparison functor for EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 99
diff changeset
52 emkobj b = record {
324511654f23 add Comparison functor for EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 99
diff changeset
53 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
54 } where
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 identity1 = ?
324511654f23 add Comparison functor for EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 99
diff changeset
57 eval1 : ?
324511654f23 add Comparison functor for EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 99
diff changeset
58 eval1 = ?
98
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
59
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)
324511654f23 add Comparison functor for EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 99
diff changeset
61 emkmap {a} {b} f = record { EMap = FMap U f ; homomorphism = homomorphism1
324511654f23 add Comparison functor for EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 99
diff changeset
62 } where
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 homomorphism1 = ?
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
121
324511654f23 add Comparison functor for EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 99
diff changeset
76 identity : {a : Obj A} → B [ emkmap (K-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
77 identity {a} = let open ≈-Reasoning (B) in
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
78 begin
121
324511654f23 add Comparison functor for EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 99
diff changeset
79 emkmap (K-id {a})
324511654f23 add Comparison functor for EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 99
diff changeset
80 ≈⟨ ? ⟩
324511654f23 add Comparison functor for EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 99
diff changeset
81 id1 B (FObj F^K a)
98
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
82 ∎
121
324511654f23 add Comparison functor for EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 99
diff changeset
83 ≈-cong : {a b : Obj A} -> {f g : EMHom a b} → A [ KMap f ≈ KMap g ] → B [ emkmap f ≈ emkmap g ]
98
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
84 ≈-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
85 begin
121
324511654f23 add Comparison functor for EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 99
diff changeset
86 emkmap f
324511654f23 add Comparison functor for EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 99
diff changeset
87 ≈⟨ ? ⟩
324511654f23 add Comparison functor for EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 99
diff changeset
88 emkmap g
98
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
89 ∎
121
324511654f23 add Comparison functor for EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 99
diff changeset
90 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
91 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
92 begin
121
324511654f23 add Comparison functor for EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 99
diff changeset
93 emkmap (g * f)
324511654f23 add Comparison functor for EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 99
diff changeset
94 ≈⟨ ? ⟩
324511654f23 add Comparison functor for EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 99
diff changeset
95 emkmap g o 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