Abstract: Within the framework of categorical logic or categorical type theory, predicate logics and type theories are understood as fibrations with structure. Fibrations, or fibred categories, provide an abstract account of the notions of indexing and substitution. These notions are central to the interpretations of predicate logics and type theories with dependent types or polymorphism. In these systems, predicates/dependent types are indexed by the contexts which declare the types of their free variables, and there is an operation of substitution of terms for free variables.
With this setting, it is natural to give a category-theoretic account of certain logical issues in terms of fibrations. In this thesis we explore logical predicates for simply typed theories, induction principles for inductive data types, and indeterminate elements for fibrations in relation to polymorphic lambda-calculi.
The notion of logical predicate is a useful tool in the study of type theories like simply typed lambda-calculus. For a categorical account of this concept, we are led to study certain structures of fibred categories. In particular, the kind of structure involved in the interpretation of simply typed lambda-calculus, namely cartesian closure, is expressed in terms of adjunctions. Hence we are led to consider adjunctions between fibred categories. We give a characterisation of these adjunctions which allows us to provide structure, given by adjunctions, to a fibred category in terms of appropriate structure on its base and its fibres.
By expressing the abovementioned categorical structure logically, in the internal language of a fibration, we can give an account of logical predicates for a cartesian closed category. By recourse to the internal language, we regard a fibred category as a category of predicates. With the same method, we provide a categorical interpretation of the induction principle for inductive data types, given by initial algebras for endofunctors on a distributive category.
We also consider the problem of adjoining indeterminate elements to fibrations. The category-theoretic concept of indeterminate or generic element captures the notion of parameter. Lambek applied this concept to characterise a functional completeness property of simply typed lambda-calculus or, equivalently, of cartesian closed categories. He showed that cartesian categories with indeterminate elements correspond to Kleisli categories for suitable comonads. Here we generalise this result to account for indeterminates for cartesian objects in a 2-category with suitable structure. To specialise this 2-categorical formulation of objects with indeterminates via Kleisli objects to the 2-category Fib of fibrations over arbitrary bases, we are led to show the existence of Kleisli objects for fibred comonads. These results provide us with the appropriate machinery to study functional completeness for polymorphic lambda-calculi by means of fibrations with indeterminates. These are also applied to give a semantics to ML module features: signatures, structures and functors.
PhD Thesis - Price £8.00
LFCS report ECS-LFCS-93-277 (also published as CST-103-93)Previous | Index | Next