The justification of identity elimination in Martin-Löf's type theory

DOI10.1007/s11245-017-9509-1zbMath1428.03045OpenAlexW2750733036MaRDI QIDQ2288279

Ansten Mørch Klev

Publication date: 17 January 2020

Published in: Topoi (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s11245-017-9509-1

zbMATH Keywords

type theoryidentityjustification of logical laws

Mathematics Subject Classification ID

Philosophical and critical aspects of logic and foundations (03A05) Type theory (03B38)

Related Items

Dialogues, Reasons and Endorsement

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• On the strength of dependent products in the type theory of Martin-Löf
• Inductive families
• Identity in Homotopy Type Theory, Part I: The Justification of Path Induction
• Does Homotopy Type Theory Provide a Foundation for Mathematics?
• A Short Scientific Autobiography
• CATEGORICAL HARMONY AND PATH INDUCTION
• Homotopy Type Theory: Univalent Foundations of Mathematics
• The inconsistency of certain formal logics