Universal Structure and a Categorical Framework for Type Theory

This thesis investigates the possibility of a computer checked language for categories with extra structure; the language is to describe objects and morphisms of those categories and to reason about them. We do so first by developing an abstract analysis of representability. This is followed by the investigation of a categorical framework for studying type theory. Our computer checked language therefore allows us to reason about the semantics of programming languages and models of logics. In order to provide our computer checked language, we need to classify categories with extra structure. Traditionally, that has been done in terms of equational structure, or more generally, essentially algebraic structure. That has proved to be somewhat awkward, both conceptually and computationally, so we give an alternative development of categories with extra structure in terms of universal structure, universality being the most important and most central concept of category theory. This unifies many of the concepts of the category theory, in particular many of those of greatest interest to computer scientists, such as cartesian closed structure, fibrations with extra structure, limits, colimits, and natural numbers objects. We use our definition of universal structure to develop a computer checked language in the proof system LEGO. We further give an abstract development of universal structure by showing how the concept of fibrations with extra structure may be seen in terms of universal structure. We continue by an investigation of the use of category theory within computer science. One of the principle uses, perhaps the deepest use, is to provide a semantics for type theory. We give a unified treatment of those categories with extra structure that are needed for the semantics of type theory, thus allowing us to use our computer checked language to reason about the semantics of programs, via use of the underlying type theory of a programming language. It also allows us a semantic study of logics, via use of their corresponding type theories as given by the Curry-Howard isomorphism. This provides what we call a categorical framework for type theory. It extends the relationship between typed lambda calculus and cartesian closed categories, allowing us, for instance, to account for dependent types, as they appear in some programming languages and proof systems such as LEGO, with its underlying type system the Extended Calculus of Constructions. Finally we illustrate our categorical framework with its universal structures by study of the fibration of 'deliverables'