*Abstract:* Theories of dependent types have been proposed
as a foundation of constructive mathematics and as a framework in
which to construct certified programs. In these applications an
important role is played by identity types which internalise
equality and therefore are essential for accommodating proofs and
programs in the same formal system.

This thesis attempts to reconcile the two different ways that type theories deal with identity types. In extensional type theory the propositional equality induced by the identity types is identified with definitional equality, i.e. conversion. This renders type-checking and well-formedness of propositions undecidable and leads to non-termination in the presence of universes. In intensional type theory propositional equality is coarser than definitional equality, the latter being confined to definitional expansion and normalisation. Then type-checking and well-formedness are decidable, and this variant is therefore adopted by most implementations.

However, the identity type in intensional type theory is not
powerful enough for formalisation of mathematics and program
development. Notably, it does not identify pointwise equal
functions (functional extensionality) and provides no means of
redefining equality on a type as a given relation, i.e. quotient
types. We call such capabilities *extensional concepts*. Other
extensional concepts of interest are uniqueness of proofs and more
specifically of equality proofs, subset types, and propositional
extensionality---the identification of equivalent propositions. In
this work we investigate to what extent these extensional concepts
may be added to intensional type theory without sacrificing
decidability and existence of canonical forms. The method we use is
the translation of identity types into equivalence relations
defined by induction on the type structure. In this way type theory
with extensional concepts can be understood as a high-level
language for working with equivalence relations instead of
equality. Such translations of type theory into itself turn out to
be best described using categorical models of type theory.

We thus begin with a thorough treatment of categorical models with particular emphasis on the interpretation of type-theoretic syntax in such models. We then show how pairs of types and predicates can be organised into a model of type theory in which subset types are available and in which any two proofs of a proposition are equal. This model has applications in the areas of program extraction from proofs and modules for functional programs. For us its main purpose is to clarify the idea of syntactic translations via categorical model constructions.

The main result of the thesis consists of the construction of two models in which functional extensionality and quotient types are available. In the first one types are modelled by types together with proposition-valued partial equivalence relations. This model is rather simple and in addition provides subset types and propositional extensionality. However, it does not furnish proper dependent types such as vectors or matrices. We try to overcome this disadvantage by using another model based on families of type-valued equivalence relations which is however much more complicated and validates certain conversion rules only up to propositional equality.

We illustrate the use of these models by several small examples taken from both formalised mathematics and program development.

We also establish various syntactic properties of propositional equality including a proof of the undecidability of typing in extensional type theory and a correspondence between derivations in extensional type theory and terms in intensional type theory with extensional concepts added. Furthermore we settle affirmatively the hitherto open question of the independence of unicity of equality proofs in intensional type theory which implies that the addition of pattern matching to intensional type theory does not yield a conservative extension.

**ECS-LFCS-95-327**, July 1995.

This report is available in the following formats:

Previous | Index | Next