Towards a Readable Formalisation of Category Theory
Greg O’Keefe · Electronic Notes in Theoretical Computer Science · 2004
We formally develop category theory up to Yoneda's lemma, using Isabelle/HOL/Isar, and survey previous formalisations. By using recently added Isabelle features, we have produced a formal text that more closely approximates informal mathematics.