uu.seUppsala University Publications
Change search
ReferencesLink to record
Permanent link

Direct link
On the strength of dependent products in the type theory of Martin-Lof
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Mathematics.
2009 (English)In: Annals of Pure and Applied Logic, ISSN 0168-0072, E-ISSN 1873-2461, Vol. 160, no 1, 1-12 p.Article in journal (Refereed) Published
Abstract [en]

One may formulate the dependent product types of Martin-Lof 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 ill 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 all alternative formulation which rectifies this deficiency. (C) 2009 Elsevier B.V. All rights reserved.

Place, publisher, year, edition, pages
2009. Vol. 160, no 1, 1-12 p.
Keyword [en]
Dependent type theory, Dependent products, Function extensionality
National Category
URN: urn:nbn:se:uu:diva-129025DOI: 10.1016/j.apal.2008.12.003ISI: 000266648600001OAI: oai:DiVA.org:uu-129025DiVA: diva2:337475
Available from: 2010-08-06 Created: 2010-08-05 Last updated: 2010-08-06Bibliographically approved

Open Access in DiVA

No full text

Other links

Publisher's full text
By organisation
Department of Mathematics
In the same journal
Annals of Pure and Applied Logic

Search outside of DiVA

GoogleGoogle Scholar
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

Altmetric score

Total: 178 hits
ReferencesLink to record
Permanent link

Direct link