Category Theory to Yoneda's Lemma

Greg O’Keefe 🌐

April 21, 2005

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.

License

GNU Lesser General Public License (LGPL)

History

April 23, 2010
The definition of the constant equinumerous was slightly too weak in the original submission and has been fixed in revision 8c2b5b3c995f.

Topics

Session Category

Cite

× 
@article{Category-AFP,
  author  = {Greg O'Keefe},
  title   = {Category Theory to Yoneda's Lemma},
  journal = {Archive of Formal Proofs},
  month   = {April},
  year    = {2005},
  note    = {\url{https://isa-afp.org/entries/Category.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download

Download

× Download latest

Older releases: