Mercurial > hg > Members > kono > Proof > category

comparison nat.agda @ 68:829e0698f87f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
join implicit parameter
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 25 Jul 2013 13:56:16 +0900
parents 51f653bd9656
children 84a150c980ce
comparison
equal deleted inserted replaced
67:e75436075bf0 68:829e0698f87f
91 { μ : NTrans A A (T ○ T) T } 91 { μ : NTrans A A (T ○ T) T }
92 { a : Obj A } ( b : Obj A ) 92 { a : Obj A } ( b : Obj A )
93 ( f : Hom A a ( FObj T b) ) 93 ( f : Hom A a ( FObj T b) )
94 ( m : Monad A T η μ ) 94 ( m : Monad A T η μ )
95 { k : Kleisli A T η μ m} 95 { k : Kleisli A T η μ m}
96 → A [ join k b (TMap η b) f ≈ f ] 96 → A [ join k (TMap η b) f ≈ f ]
97 Lemma7 c {T} η b f m {k} = 97 Lemma7 c {T} η b f m {k} =
98 let open ≈-Reasoning (c) 98 let open ≈-Reasoning (c)
99 μ = mu ( monad k ) 99 μ = mu ( monad k )
100 in 100 in
101 begin 101 begin
102 join k b (TMap η b) f 102 join k (TMap η b) f
103 ≈⟨ refl-hom ⟩ 103 ≈⟨ refl-hom ⟩
104 c [ TMap μ b o c [ FMap T ((TMap η b)) o f ] ] 104 c [ TMap μ b o c [ FMap T ((TMap η b)) o f ] ]
105 ≈⟨ IsCategory.associative (Category.isCategory c) ⟩ 105 ≈⟨ IsCategory.associative (Category.isCategory c) ⟩
106 c [ c [ TMap μ b o FMap T ((TMap η b)) ] o f ] 106 c [ c [ TMap μ b o FMap T ((TMap η b)) ] o f ]
107 ≈⟨ car ( IsMonad.unity2 ( isMonad ( monad k )) ) ⟩ 107 ≈⟨ car ( IsMonad.unity2 ( isMonad ( monad k )) ) ⟩
117 { μ : NTrans A A (T ○ T) T } 117 { μ : NTrans A A (T ○ T) T }
118 ( a : Obj A ) ( b : Obj A ) 118 ( a : Obj A ) ( b : Obj A )
119 ( f : Hom A a ( FObj T b) ) 119 ( f : Hom A a ( FObj T b) )
120 ( m : Monad A T η μ ) 120 ( m : Monad A T η μ )
121 ( k : Kleisli A T η μ m) 121 ( k : Kleisli A T η μ m)
122 → A [ join k b f (TMap η a) ≈ f ] 122 → A [ join k f (TMap η a) ≈ f ]
123 Lemma8 c T η a b f m k = 123 Lemma8 c T η a b f m k =
124 begin 124 begin
125 join k b f (TMap η a) 125 join k f (TMap η a)
126 ≈⟨ refl-hom ⟩ 126 ≈⟨ refl-hom ⟩
127 c [ TMap μ b o c [ FMap T f o (TMap η a) ] ] 127 c [ TMap μ b o c [ FMap T f o (TMap η a) ] ]
128 ≈⟨ cdr ( nat η ) ⟩ 128 ≈⟨ cdr ( nat η ) ⟩
129 c [ TMap μ b o c [ (TMap η ( FObj T b)) o f ] ] 129 c [ TMap μ b o c [ (TMap η ( FObj T b)) o f ] ]
130 ≈⟨ IsCategory.associative (Category.isCategory c) ⟩ 130 ≈⟨ IsCategory.associative (Category.isCategory c) ⟩
146 ( f : Hom A a ( FObj T b) ) 146 ( f : Hom A a ( FObj T b) )
147 ( g : Hom A b ( FObj T c) ) 147 ( g : Hom A b ( FObj T c) )
148 ( h : Hom A c ( FObj T d) ) 148 ( h : Hom A c ( FObj T d) )
149 ( m : Monad A T η μ ) 149 ( m : Monad A T η μ )
150 { k : Kleisli A T η μ m} 150 { k : Kleisli A T η μ m}
151 → A [ join k d h (join k c g f) ≈ join k d ( join k d h g) f ] 151 → A [ join k h (join k g f) ≈ join k ( join k h g) f ]
152 Lemma9 A {T} {η} {μ} {a} {b} {c} {d} f g h m {k} = 152 Lemma9 A {T} {η} {μ} {a} {b} {c} {d} f g h m {k} =
153 begin 153 begin
154 join k d h (join k c g f) 154 join k h (join k g f)
155 ≈⟨⟩ 155 ≈⟨⟩
156 join k d h ( ( TMap μ c o ( FMap T g o f ) ) ) 156 join k h ( ( TMap μ c o ( FMap T g o f ) ) )
157 ≈⟨ refl-hom ⟩ 157 ≈⟨ refl-hom ⟩
158 ( TMap μ d o ( FMap T h o ( TMap μ c o ( FMap T g o f ) ) ) ) 158 ( TMap μ d o ( FMap T h o ( TMap μ c o ( FMap T g o f ) ) ) )
159 ≈⟨ cdr ( cdr ( assoc )) ⟩ 159 ≈⟨ cdr ( cdr ( assoc )) ⟩
160 ( TMap μ d o ( FMap T h o ( ( TMap μ c o FMap T g ) o f ) ) ) 160 ( TMap μ d o ( FMap T h o ( ( TMap μ c o FMap T g ) o f ) ) )
161 ≈⟨ assoc ⟩ --- ( f o ( g o h ) ) = ( ( f o g ) o h ) 161 ≈⟨ assoc ⟩ --- ( f o ( g o h ) ) = ( ( f o g ) o h )
196 ≈⟨ sym assoc ⟩ 196 ≈⟨ sym assoc ⟩
197 ( TMap μ d o ( ( FMap T ( TMap μ d ) o FMap T ( ( FMap T h o g ) ) ) o f ) ) 197 ( TMap μ d o ( ( FMap T ( TMap μ d ) o FMap T ( ( FMap T h o g ) ) ) o f ) )
198 ≈⟨ cdr ( car ( sym ( distr T ))) ⟩ 198 ≈⟨ cdr ( car ( sym ( distr T ))) ⟩
199 ( TMap μ d o ( FMap T ( ( ( TMap μ d ) o ( FMap T h o g ) ) ) o f ) ) 199 ( TMap μ d o ( FMap T ( ( ( TMap μ d ) o ( FMap T h o g ) ) ) o f ) )
200 ≈⟨ refl-hom ⟩ 200 ≈⟨ refl-hom ⟩
201 join k d ( ( TMap μ d o ( FMap T h o g ) ) ) f 201 join k ( ( TMap μ d o ( FMap T h o g ) ) ) f
202 ≈⟨ refl-hom ⟩ 202 ≈⟨ refl-hom ⟩
203 join k d ( join k d h g) f 203 join k ( join k h g) f
204 ∎ where open ≈-Reasoning (A) 204 ∎ where open ≈-Reasoning (A)
205 205
206 -- Kleisli-join : {!!} 206 -- Kleisli-join : {!!}
207 -- Kleisli-join = {!!} 207 -- Kleisli-join = {!!}
208 208