*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)*