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

DOI10.1093/PHILMAT/NKV014MaRDI QIDQ2965632zbMATHOpenAlexFDO

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

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)

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?

Cited in

(13)

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

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)