Mercurial > hg > Members > kono > Proof > category

comparison em-category.agda @ 100:59dec035602c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Eilenberg-Moore Category start
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 30 Jul 2013 17:58:20 +0900
parents
children 0f7086b6a1a6
comparison
equal deleted inserted replaced
99:bd542a1caf08 100:59dec035602c
1 -- -- -- -- -- -- -- --
2 -- Monad to Eilenberg-Moore Category
3 -- defines U^T and F^T as a resolution of Monad
4 -- checks Adjointness
5 --
6 -- Shinji KONO <kono@ie.u-ryukyu.ac.jp>
7 -- -- -- -- -- -- -- --
8
9 -- Monad
10 -- Category A
11 -- A = Category
12 -- Functor T : A → A
13 --T(a) = t(a)
14 --T(f) = tf(f)
15
16 open import Category -- https://github.com/konn/category-agda
17 open import Level
18 --open import Category.HomReasoning
19 open import HomReasoning
20 open import cat-utility
21 open import Category.Cat
22
23 module em-category { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ }
24 { T : Functor A A }
25 { η : NTrans A A identityFunctor T }
26 { μ : NTrans A A (T ○ T) T }
27 { M : Monad A T η μ } where
28
29 --
30 -- Hom in Eilenberg-Moore Category
31 --
32
33 record IsEMAlgebra { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } { T : Functor A A }
34 (a : Obj A) (φ : FObj T a -> a ) : Set c₁
35 field
36 identity : A [ A [ φ o TMap η a ] ≈ id1 A a ]
37 eval : A [ A [ φ o TMap μ a ] ≈ A [ φ o FMap T φ ]
38 open IsEMAlgebra
39
40 record EMAlgebra { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } { T : Functor A A }
41 (a : Obj A) (φ : FObj T a -> a ) : Set c₂
42 field
43 isEMAlbgebra : IsEMAlgebra {c₁} {c₂} {ℓ} {A} {T} a φ
44 open EMAlgebra
45
46 data EMObj { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } { T : Functor A A }
47 {a : Obj A} {φ : FObj T a -> a } {EMAlgebra a φ} : Set ( c₁ ⊔ c₂ )
48 emObj : (IsEMAlgebra a φ) -> EMObj {_} {_} {_} {_} {_} {a} {φ}
49
50 record IsEMHom { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } { T : Functor A A }
51 (a : EMObj {c₁} {c₂} {ℓ} {A} {T} x φ )
52 (b : EMObj {c₁} {c₂} {ℓ} {A} {T} y φ' ) : Set c₂ where
53 field
54 homomorphism : A [ φ' o FMap T α ] ≈ A [ α o φ ] ]
55 open IsEMHom
56
57 record EMHom { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } { T : Functor A A }
58 (a : EMObj {c₁} {c₂} {ℓ} {A} {T} x)
59 (b : EMObj {c₁} {c₂} {ℓ} {A} {T} y) : Set c₂ where
60 field
61 EMap : Hom A x y
62 isEMHom : IsEMHom {c₁} {c₂} {ℓ} {A} {T} a b
63 open EMHom
64
65 EM-id : {x : Obj A} a : EMObj EMObj {_} {_} {_} {_} {_} {a}) -> EMHom a a
66 EM-id {x = x} _ = record { EMap = id1 A x ; isEMHom = Lemma-EM1 x }
67
68 open import Relation.Binary.Core
69
70 _≗_ : { a : EMObj } { b : EMObj } (f g : EMHom a b ) -> Set ℓ
71 _≗_ {a} {b} f g = A [ EMap f ≈ EMap g ]
72
73 _∙_ : { a b : EMObj A } → { c : EMObj A } →
74 ( EMHom b c) → ( EMHom a b) → EMHom a c
75 _∙_ {a} {b} {c} g f = record { EMap = A [ (EMap g) o (EMap f) ; isEMHom = Lemma-EM2 a b c g f }
76
77 isEilenberg-MooreCategory : IsCategory ( Obj A ) EMHom _⋍_ _*_ EM-id
78 isEilenberg-MooreCategory = record { isEquivalence = isEquivalence
79 ; identityL = KidL
80 ; identityR = KidR
81 ; o-resp-≈ = Ko-resp
82 ; associative = Kassoc
83 }
84 where
85 open ≈-Reasoning (A)
86 isEquivalence : { a b : Obj A } ->
87 IsEquivalence {_} {_} {EMHom a b} _⋍_
88 isEquivalence {C} {D} = -- this is the same function as A's equivalence but has different types
89 record { refl = refl-hom
90 ; sym = sym
91 ; trans = trans-hom
92 }
93 KidL : {C D : Obj A} -> {f : EMHom C D} → (EM-id * f) ⋍ f
94 KidL {_} {_} {f} = Lemma7 (EMap f)
95 KidR : {C D : Obj A} -> {f : EMHom C D} → (f * EM-id) ⋍ f
96 KidR {_} {_} {f} = Lemma8 (EMap f)
97 Ko-resp : {a b c : Obj A} -> {f g : EMHom a b } → {h i : EMHom b c } →
98 f ⋍ g → h ⋍ i → (h * f) ⋍ (i * g)
99 Ko-resp {a} {b} {c} {f} {g} {h} {i} eq-fg eq-hi = Lemma10 {a} {b} {c} (EMap f) (EMap g) (EMap h) (EMap i) eq-fg eq-hi
100 Kassoc : {a b c d : Obj A} -> {f : EMHom c d } → {g : EMHom b c } → {h : EMHom a b } →
101 (f * (g * h)) ⋍ ((f * g) * h)
102 Kassoc {_} {_} {_} {_} {f} {g} {h} = Lemma9 (EMap f) (EMap g) (EMap h)
103
104 Eilenberg-MooreCategory : Category c₁ c₂ ℓ
105 Eilenberg-MooreCategory =
106 record { Obj = Obj A
107 ; Hom = EMHom
108 ; _o_ = _*_
109 ; _≈_ = _⋍_
110 ; Id = EM-id
111 ; isCategory = isEilenberg-MooreCategory
112 }
113
114 --
115 -- Resolution
116 -- T = U_T U_F
117 -- nat-ε
118 -- nat-η
119 --
120 --
121 --
122 -- U_T : Functor Eilenberg-MooreCategory A
123 -- U_T = record {
124 -- FObj = FObj T
125 -- ; FMap = ufmap
126 -- ; isFunctor = record
127 -- { ≈-cong = ≈-cong
128 -- ; identity = identity
129 -- ; distr = distr1
130 -- }
131 -- } where
132 -- identity : {a : Obj A} → A [ ufmap (EM-id {a}) ≈ id1 A (FObj T a) ]
133 -- identity {a} = let open ≈-Reasoning (A) in
134 -- begin
135 -- TMap μ (a) o FMap T (TMap η a)
136 -- ≈⟨ IsMonad.unity2 (isMonad M) ⟩
137 -- id1 A (FObj T a)
138 -- ∎
139 -- ≈-cong : {a b : Obj A} {f g : EMHom a b} → A [ EMap f ≈ EMap g ] → A [ ufmap f ≈ ufmap g ]
140 -- ≈-cong {a} {b} {f} {g} f≈g = let open ≈-Reasoning (A) in
141 -- begin
142 -- TMap μ (b) o FMap T (EMap f)
143 -- ≈⟨ cdr (fcong T f≈g) ⟩
144 -- TMap μ (b) o FMap T (EMap g)
145 -- ∎
146 -- distr1 : {a b c : Obj A} {f : EMHom a b} {g : EMHom b c} → A [ ufmap (g * f) ≈ (A [ ufmap g o ufmap f ] )]
147 -- distr1 {a} {b} {c} {f} {g} = let open ≈-Reasoning (A) in
148 -- begin
149 -- ufmap (g * f)
150 -- ≈⟨⟩
151 -- ufmap {a} {c} ( record { EMap = TMap μ (c) o (FMap T (EMap g) o (EMap f)) } )
152 -- ≈⟨⟩
153 -- TMap μ (c) o FMap T ( TMap μ (c) o (FMap T (EMap g) o (EMap f)))
154 -- ≈⟨ cdr ( distr T) ⟩
155 -- TMap μ (c) o (( FMap T ( TMap μ (c)) o FMap T (FMap T (EMap g) o (EMap f))))
156 -- ≈⟨ assoc ⟩
157 -- (TMap μ (c) o ( FMap T ( TMap μ (c)))) o FMap T (FMap T (EMap g) o (EMap f))
158 -- ≈⟨ car (sym (IsMonad.assoc (isMonad M))) ⟩
159 -- (TMap μ (c) o ( TMap μ (FObj T c))) o FMap T (FMap T (EMap g) o (EMap f))
160 -- ≈⟨ sym assoc ⟩
161 -- TMap μ (c) o (( TMap μ (FObj T c)) o FMap T (FMap T (EMap g) o (EMap f)))
162 -- ≈⟨ cdr (cdr (distr T)) ⟩
163 -- TMap μ (c) o (( TMap μ (FObj T c)) o (FMap T (FMap T (EMap g)) o FMap T (EMap f)))
164 -- ≈⟨ cdr (assoc) ⟩
165 -- TMap μ (c) o ((( TMap μ (FObj T c)) o (FMap T (FMap T (EMap g)))) o FMap T (EMap f))
166 -- ≈⟨ sym (cdr (car (nat μ ))) ⟩
167 -- TMap μ (c) o ((FMap T (EMap g ) o TMap μ (b)) o FMap T (EMap f ))
168 -- ≈⟨ cdr (sym assoc) ⟩
169 -- TMap μ (c) o (FMap T (EMap g ) o ( TMap μ (b) o FMap T (EMap f )))
170 -- ≈⟨ assoc ⟩
171 -- ( TMap μ (c) o FMap T (EMap g ) ) o ( TMap μ (b) o FMap T (EMap f ) )
172 -- ≈⟨⟩
173 -- ufmap g o ufmap f
174 -- ∎
175 --
176 -- open MResolution
177 --
178 -- Resolution_T : MResolution A Eilenberg-MooreCategory T U_T F_T {nat-η} {nat-ε} {nat-μ} Adj_T
179 -- Resolution_T = record {
180 -- T=UF = Lemma11;
181 -- μ=UεF = Lemma12
182 -- }
183 --
184 -- -- end