Martin Hofmann (1995)

# Conservativity of Equality Reflection over Intensional Type Theory

In: Types for Proofs and Programs, International Workshop TYPES'95, Torino, Italy, June 5-8, 1995, Selected Papers, ed. by Stefano Berardi and Mario Coppo, vol. 1158, pp. 153-164, Springer. Lecture Notes in Computer Science (ISBN: 3-540-61780-9).

We investigate the relationship between intensional and extensional formulations of Martin-Löf type theory. We exhibit two principles which are not provable in the intensional formulation: uniqueness of identity and functional extensionality. We show that extensional type theory is conservative over the intensional one extended by these two principles, meaning that the same types are inhabited, whenever they make sense. The proof is non-constructive because it uses set-theoretic quotienting and choice of representatives.

Document Actions