Mercurial > hg > Members > kono > Proof > category
comparison nat.agda @ 21:a7b0f7ab9881
unity law 1
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 12 Jul 2013 13:39:33 +0900 |
| parents | 93c0a2565d53 |
| children | b3cb592d7b9d |
comparison
equal
deleted
inserted
replaced
| 20:e34c93046acf | 21:a7b0f7ab9881 |
|---|---|
| 177 c [ Id {_} {_} {_} {c} b o g ] | 177 c [ Id {_} {_} {_} {c} b o g ] |
| 178 ≈⟨ IsCategory.identityL (Category.isCategory c) ⟩ | 178 ≈⟨ IsCategory.identityL (Category.isCategory c) ⟩ |
| 179 g | 179 g |
| 180 ∎ | 180 ∎ |
| 181 | 181 |
| 182 lemma70 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) {a b c : Obj A } {x y : Hom A a b } ( f : Hom A c a ) -> | |
| 183 A [ x ≈ y ] -> A [ A [ x o f ] ≈ A [ y o f ] ] | |
| 184 lemma70 c f eq = ( IsCategory.o-resp-≈ ( Category.isCategory c )) ( ≈-Reasoning.refl-hom c ) eq | |
| 185 | |
| 182 open Kleisli | 186 open Kleisli |
| 183 Lemma7 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) -> | 187 Lemma7 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) -> |
| 184 { T : Functor A A } | 188 ( T : Functor A A ) |
| 185 { η : NTrans A A identityFunctor T } | 189 ( η : NTrans A A identityFunctor T ) |
| 186 { μ : NTrans A A (T ○ T) T } | 190 { μ : NTrans A A (T ○ T) T } |
| 187 { a b : Obj A } | 191 { a : Obj A } ( b : Obj A ) |
| 188 { f : Hom A a ( FObj T b) } | 192 ( f : Hom A a ( FObj T b) ) |
| 189 { M : Monad A T η μ } | 193 ( M : Monad A T η μ ) |
| 190 ( K : Kleisli A T η μ M) | 194 ( K : Kleisli A T η μ M) |
| 191 -> A [ join K b (Trans η b) f ≈ f ] | 195 -> A [ join K b (Trans η b) f ≈ f ] |
| 192 Lemma7 c k = | 196 Lemma7 c T η b f m k = |
| 193 -- { a b : Obj c} | 197 let open ≈-Reasoning (c) |
| 194 -- { T : Functor c c } | 198 μ = mu ( monad k ) |
| 195 -- { η : NTrans c c identityFunctor T } | 199 in |
| 196 -- { f : Hom c a ( FObj T b) } | 200 begin |
| 197 {!!} | 201 join k b (Trans η b) f |
| 198 | 202 ≈⟨ refl-hom ⟩ |
| 203 c [ Trans μ b o c [ FMap T ((Trans η b)) o f ] ] | |
| 204 ≈⟨ IsCategory.associative (Category.isCategory c) ⟩ | |
| 205 c [ c [ Trans μ b o FMap T ((Trans η b)) ] o f ] | |
| 206 ≈⟨ lemma70 c f ( IsMonad.unity2 ( isMonad ( monad k )) ) ⟩ | |
| 207 c [ Id {_} {_} {_} {c} (FObj T b) o f ] | |
| 208 ≈⟨ IsCategory.identityL (Category.isCategory c) ⟩ | |
| 209 f | |
| 210 ∎ | |
| 199 | 211 |
| 200 Lemma8 : {c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ} | 212 Lemma8 : {c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ} |
| 201 { T : Functor A A } | 213 { T : Functor A A } |
| 202 { η : NTrans A A identityFunctor T } | 214 { η : NTrans A A identityFunctor T } |
| 203 { μ : NTrans A A (T ○ T) T } | 215 { μ : NTrans A A (T ○ T) T } |