Martin Hofmann (1993)

# Elimination of Extensionality in Martin-Löf Type Theory

In: Types for Proofs and Programs, International Workshop TYPES'93, Nijmegen, The Netherlands, May 24-28, 1993, Selected Papers, ed. by Henk Barendregt and Tobias Nipkow, vol. 806, pp. 166-190, Springer. Lecture Notes in Computer Science (ISBN: 3-540-58085-9).

We construct a syntactic model of intensional Martin-Löf type theory in which two pointwise propositionally equal functions are propositionally equal themselves. In the model types are 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.

Document Actions