Skip navigation
Skip navigation

Towards a readable formalisation of category theory

O'Keefe, Greg


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.

CollectionsANU Research Publications
Date published: 2004
Type: Journal article
Source: Electronic Notes in Theoretical Computer Science
DOI: 10.1016/j.entcs.2003.12.014


File Description SizeFormat Image
01_O'Keefe_Towards_a_readable_2004.pdf228.95 kBAdobe PDF    Request a copy

Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.

Updated:  19 May 2020/ Responsible Officer:  University Librarian/ Page Contact:  Library Systems & Web Coordinator