Identity in homotopy type theory. Part I: The justification of path induction

DOI10.1093/PHILMAT/NKV014zbMATH Open1380.03027OpenAlexW2221380295MaRDI QIDQ2965632FDOQ2965632

Authors: James Ladyman, Stuart Presnell 

Publication date: 3 March 2017

Published in: Philosophia Mathematica (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1093/philmat/nkv014

Recommendations

• CATEGORICAL HARMONY AND PATH INDUCTION
• Identity in homotopy type theory. II: The conceptual and philosophical status of identity in HoTT
• A meaning explanation for HoTT
• Homotopy Type Theory
• Does homotopy type theory provide a foundation for mathematics?

zbMATH Keywords

homotopy type theory

Mathematics Subject Classification ID

Philosophical and critical aspects of logic and foundations (03A05) Categorical logic, topoi (03G30) Topological categories, foundations of homotopy theory (55U40)

Cited In (13)

• The hole argument in homotopy type theory
• The hole argument, take \(n\)
• Topological quantum gates in homotopy type theory
• On the identity type as the type of computational paths
• Venus homotopically
• The justification of identity elimination in Martin-Löf's type theory
• A meaning explanation for HoTT
• CATEGORICAL HARMONY AND PATH INDUCTION
• UNIVERSES AND UNIVALENCE IN HOMOTOPY TYPE THEORY
• Modal Homotopy Type Theory
• Representation and Spacetime: The Hole Argument Revisited
• Identity in homotopy type theory. II: The conceptual and philosophical status of identity in HoTT
• Observability in the univalent universe

This page was built for publication: Identity in homotopy type theory. Part I: The justification of path induction

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2965632)