Abstract
This development proves Yoneda's lemma and aims to be readable by humans. It only defines what is needed for the lemma: categories, functors and natural transformations. Limits, adjunctions and other important concepts are not included.
GNU Lesser General Public License (LGPL)Change history
[2010-04-23] The definition of the constant equinumerous was slightly too weak in the original submission and has been fixed in revision 8c2b5b3c995f.