A Formal Calculus for Categories
Mario José Cáccamo June 2003 |

## Abstract:
This dissertation studies the logic underlying category theory.
In particular we present a formal calculus for reasoning about universal
properties. The aim is to systematise judgements about
functoriality
and naturality central to categorical reasoning. The calculus is based
on a language which extends the typed lambda calculus with new binders to
represent universal constructions. The types of the languages are interpreted
as locally small categories and the expressions represent functors.
The logic supports a syntactic treatment of universality and duality.
Contravariance requires a definition of universality generous enough to deal
with functors of mixed variance.
The equational theory of the
lambda calculus is extended with new rules for the definitions of universal
properties. These judgements express the existence of natural isomorphisms
between functors. The isomorphisms allow us to formalise in the calculus
results like the Yoneda lemma and Fubini theorem for ends. The definitions of
limits and ends are given as
The presence of
structural rules as primitive in the calculus together with the rule for
duality give rise to issues concerning the Finally, we investigate how to generalise the calculus to enriched categories. Here we lose the ability to manipulate contexts through weakening and contraction and conical limits are not longer adequate.
Available as |

Last modified: 2004-07-06 by webmaster.