Mercurial > hg > Members > kono > Proof > category
log universal-mapping.agda @ 328:d6eb3520ccf8
| age | author | description |
|---|---|---|
| 2013-09-29 | Shinji KONO | arrow and lambda fix |
| 2013-08-25 | Shinji KONO | comment |
| 2013-08-25 | Shinji KONO | hom set adjunction done. |
| 2013-08-24 | Shinji KONO | hom-set to universal mapping done. |
| 2013-08-24 | Shinji KONO | add more axiom on unity of oppsite |
| 2013-08-23 | Shinji KONO | hmmmm |
| 2013-08-23 | Shinji KONO | hmm |
| 2013-08-23 | Shinji KONO | unity of oppsite |
| 2013-08-18 | Shinji KONO | mmmm |
| 2013-08-08 | Shinji KONO | remove Kleisli record |
| 2013-07-25 | Shinji KONO | distr |
| 2013-07-24 | Shinji KONO | add unitility |
| 2013-07-23 | Shinji KONO | Adjoint proved. All done. |
| 2013-07-23 | Shinji KONO | cleanup |
| 2013-07-23 | Shinji KONO | start adjunction |
| 2013-07-23 | Shinji KONO | nat-ε proved |
| 2013-07-23 | Shinji KONO | on going... |
| 2013-07-23 | Shinji KONO | on goging |
| 2013-07-23 | Shinji KONO | naturality of ε |
| 2013-07-22 | Shinji KONO | naturarity of η |
| 2013-07-22 | Shinji KONO | F is Functor proved. |
| 2013-07-22 | Shinji KONO | Functor cong done |
| 2013-07-22 | Shinji KONO | uniq-univeralMapping from Adjunction |
| 2013-07-22 | Shinji KONO | f replacement |
| 2013-07-22 | Shinji KONO | uniqness |
| 2013-07-22 | Shinji KONO | Functor Identity |
| 2013-07-22 | Shinji KONO | isFunctor |
| 2013-07-22 | Shinji KONO | Adjunction to Universal Mapping end |
| 2013-07-22 | Shinji KONO | Reasoning |
| 2013-07-22 | Shinji KONO | reasoning |
| 2013-07-22 | Shinji KONO | universalMapping |
| 2013-07-22 | Shinji KONO | isUniversalMapping |
| 2013-07-22 | Shinji KONO | f∗ = ε(b)F(f), |
| 2013-07-22 | Shinji KONO | trying... |
| 2013-07-22 | Shinji KONO | add Adj to Universal Mapping |
| 2013-07-22 | Shinji KONO | Adjoint |
| 2013-07-22 | Shinji KONO | add universal mapping |