Boulton, Richard John^{2}, Jackson, Paul Bernard^{2}

Affiliations:

^{1} Department of Computer Science, Faculty of Science, Aarhus University, Aarhus University^{2} unknown

Abstract:

A calculus for a fragment of category theory is presented. The types in the language denote categories and the expressions functors. The judgements of the calculus systematise categorical arguments such as: an expression is functorial in its free variables; two expressions are naturally isomorphic in their free variables. There are special binders for limits and more general ends. The rules for limits and ends support an algebraic manipulation of universal constructions as opposed to a more traditional diagrammatic approach. Duality within the calculus and applications in proving continuity are discussed with examples. The calculus gives a basis for mechanising a theory of categories in a generic theorem prover like Isabelle.

ISBN:

9783540425250

Type:

Conference paper

Language:

English

Published in:

Lecture Notes in Computer Science: Theorem Proving in Higher Order Logics, 2001, p. 136-153

Main Research Area:

Science/technology

Publication Status:

Published

Review type:

Peer Review

Conference:

14th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2001)