Category Theory to Yoneda's Lemma

 

Title:	Category Theory to Yoneda's Lemma
Author:	Greg O'Keefe
Submission date:	2005-04-21
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.

 

Proof outline Proof document

Browse theories

Download this entry

Older releases: Isabelle 2009: afp-Category-2009-04-29.tar.gz Isabelle 2008: afp-Category-2008-06-10.tar.gz Isabelle 2007: afp-Category-2007-11-27.tar.gz Isabelle 2005: afp-Category-2005-10-14.tar.gz Isabelle 2004: afp-Category-2005-05-01.tar.gz