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.
- April 23, 2010
- The definition of the constant equinumerous was slightly too weak in the original submission and has been fixed in revision 8c2b5b3c995f.