Elimination of extensionality in Martin-Löf type theory

Abstract

We construct a syntactic model of intensional Martin-LSf type theory in which two pointwise propositionally equal functions are propositionally equal themselves. In the model types ate interpreted as types equipped with equivalence relations; the identity type at each type is interpreted as the associated relation. The interpretation function from the syntax to the model gives rise to a procedure which replaces all instances of the identity type by suitable relations defined by induction on the type structure and thereby eliminates instances of an axiom which states that pointwise propositionally equal functions are propositionally equal themselves. We also sketch how “quotient types” can be interpreted.