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

DOI10.1016/j.apal.2008.12.003zbMath1171.03004arXiv0803.4466OpenAlexW2151011698MaRDI QIDQ1024547

Richard Garner

Publication date: 17 June 2009

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/0803.4466

zbMATH Keywords

Martin-Löf type theoryelimination ruledependent type theorydependent productsfunction extensionality

Mathematics Subject Classification ID

Intuitionistic mathematics (03F55)

Related Items

Towards a constructive simplicial model of Univalent Foundations ⋮ Homotopical inverse diagrams in categories with attributes ⋮ The simplicial model of univalent foundations (after Voevodsky) ⋮ The justification of identity elimination in Martin-Löf's type theory ⋮ Proof, meaning and paradox: some remarks ⋮ Two-dimensional models of type theory ⋮ ETA-RULES IN MARTIN-LÖF TYPE THEORY ⋮ Generalized Elimination Inferences, Higher-Level Rules, and the Implications-as-Rules Interpretation of the Sequent Calculus

Cites Work

• Constructivism in mathematics. An introduction. Volume II
• Two-dimensional models of type theory
• A natural extension of natural deduction
• Conservativity of equality reflection over intensional type theory
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item