|
A Higher-Order Calculus for Categories
Mario Jose Cáccamo
June 2001 |
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
Available as PostScript, PDF, DVI. |