log universal-mapping.agda @ 775:06a7831cf6ce

age author description
2018-06-13 Shinji KONO exchange left and right
2017-11-11 Shinji KONO fix universal mapping done.
2017-11-11 Shinji KONO fix again
2017-11-11 Shinji KONO fix monad/adjunction definition
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