Extensional Constructs in Intensional Type Theory

Theories of dependent types have been proposed as a foundation of constructive mathematics [75, 20] and as a framework in which to construct certified programs [67, 20, 112] and to extract programs from proofs [28, 90]. Using implementations of such type theories, substantial pieces of constructive mathematics have been formalised and medium scale program developments and verifications have been carried out.

In this chapter we fix a particular syntax for a dependently typed calculus and define an abstract notion of model as well as a general interpretation function mapping syntactical objects to entities in a model. This interpretation function is shown to be sound with respect to the syntax.

The main focus of this Chapter are the proofs of two important properties of extensional type theory, i.e. type theory with propositional and definitional equality identified. The first property is undecidability of this theory; in view of the information loss in the equality reflection rule an obvious thing, which is nevertheless not completely trivial to prove (Section 3.2.2). The second property is the conservativity of extensional type theory over intensional type theory with extensional constructs (Section 3.2.5). These two properties constitute the major justification for the use of intensional type theory with extensional constructs.

In this chapter we study models for quotient types and the related constructs of functional and propositional extensionality. The general method is to construct models in which types are interpreted as types together with partial equivalence relations. Propositional equality at some type is then the associated partial equivalence relation.

In this chapter we describe some small applications of the extended type theories studied in this thesis. Most of the applications only use the extensional constructs qua constants; the additional definitional equalities gained by the interpretation in the various syntactic models are not used. This allows us to carry out the examples within the existing Lego system by merely working in a context containing assumptions for the various extensional constructs (see Appendix Appendix A). Most of the examples have been carried out in Lego, but we prefer to stick to the notation used so far and not give actual Lego syntax here. The main purpose of the examples is to explain the usefulness of extensional constructs as intermediate “macro language” rather than working with setoids or deliverables directly.

We have compared extensional and intensional formulations of type theory and argued for the need for adding “extensional constructs” to the latter. These extensional constructs have been justified using syntactic models based on pure intensional type theory.