Skip navigation
Skip navigation

Towards a readable formalisation of category theory

O'Keefe, Greg

Description

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
URI: http://hdl.handle.net/1885/87600
Source: Electronic Notes in Theoretical Computer Science
DOI: 10.1016/j.entcs.2003.12.014

Download

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:  23 August 2018/ Responsible Officer:  University Librarian/ Page Contact:  Library Systems & Web Coordinator