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.
CITATION STYLE
Hofmann, M. (1996). Conservativity of equality reflection over intensional type theory. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1158 LNCS, pp. 153–164). https://doi.org/10.1007/3-540-61780-9_68
Mendeley helps you to discover research relevant for your work.