On the strength of dependent products in the type theory of Martin-Löf

Richard Garner*

*Corresponding author for this work

Research output: Contribution to journalArticlepeer-review

10 Citations (Scopus)

Abstract

One may formulate the dependent product types of Martin-Löf type theory either in terms of abstraction and application operators like those for the lambda-calculus; or in terms of introduction and elimination rules like those for the other constructors of type theory. It is known that the latter rules are at least as strong as the former: we show that they are in fact strictly stronger. We also show, in the presence of the identity types, that the elimination rule for dependent products-which is a "higher-order" inference rule in the sense of Schroeder-Heister-can be reformulated in a first-order manner. Finally, we consider the principle of function extensionality in type theory, which asserts that two elements of a dependent product type which are pointwise propositionally equal, are themselves propositionally equal. We demonstrate that the usual formulation of this principle fails to verify a number of very natural propositional equalities; and suggest an alternative formulation which rectifies this deficiency.

Original languageEnglish
Pages (from-to)1-12
Number of pages12
JournalAnnals of Pure and Applied Logic
Volume160
Issue number1
DOIs
Publication statusPublished - Jul 2009
Externally publishedYes

Keywords

  • Dependent products
  • Dependent type theory
  • Function extensionality

Fingerprint

Dive into the research topics of 'On the strength of dependent products in the type theory of Martin-Löf'. Together they form a unique fingerprint.

Cite this