A Formal Calculus for Categories

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. Ends generalise limits to cover these kinds of functors and moreover provide the basis for a very convenient algebraic manipulation of expressions.

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 representations for special Set-valued functors where Set is the category of sets and functions. This establishes the basis for a more calculational presentation of category theory rather than the traditional diagrammatic one.

The presence of structural rules as primitive in the calculus together with the rule for duality give rise to issues concerning the coherence of the system. As for every well-typed expression-in-context there are several possible derivations it is sensible to ask whether they result in the same interpretation. For the functoriality judgements the system is coherent up to natural isomorphism. In the case of naturality judgements a simple example shows its incoherence. However in many situations to know there exists a natural isomorphism is enough. As one of the contributions in this dissertation, the calculus provides a useful tool to verify that a functor is continuous by just establishing the existence of a certain natural isomorphism.

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.

Abstract: