On the strength of dependent products in the type theory of Martin-Löf
From MaRDI portal
Publication:1024547
DOI10.1016/j.apal.2008.12.003zbMath1171.03004arXiv0803.4466MaRDI QIDQ1024547
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
Martin-Löf type theory; elimination rule; dependent type theory; dependent products; function extensionality
03F55: Intuitionistic mathematics
Related Items
ETA-RULES IN MARTIN-LÖF TYPE THEORY, Generalized Elimination Inferences, Higher-Level Rules, and the Implications-as-Rules Interpretation of the Sequent Calculus, The simplicial model of univalent foundations (after Voevodsky), Homotopical inverse diagrams in categories with attributes, The justification of identity elimination in Martin-Löf's type theory, Proof, meaning and paradox: some remarks, Two-dimensional models of type theory
Cites Work