Identity in homotopy type theory: Part II, the conceptual and philosophical status of identity in HoTT

James Ladyman, Stuart Presnell

Research output: Contribution to journalArticle (Academic Journal)peer-review

2 Citations (Scopus)
393 Downloads (Pure)

Abstract

Among the most interesting features of Homotopy Type Theory (HoTT) is the way it treats identity, which has various unusual characteristics. We examine the formal features of "identity types" in HoTT, and how they relate to its other features including intensionality, constructive logic, the interpretation of types as concepts, and the Univalence Axiom. The unusual behaviour of identity types might suggest that they be reinterpreted as representing indiscernibility. We explore this by defining indiscernibility in HoTT and examine its relationship with identity. We argue that identity types are a primitive component of HoTT and cannot be reduced to indiscernibility.

Original languageEnglish
Pages (from-to)210-245
Number of pages36
JournalPhilosophia Mathematica
Volume25
Issue number2
Early online date15 Dec 2016
DOIs
Publication statusPublished - 1 Jun 2017

Structured keywords

  • Centre for Science and Philosophy
  • Centre_for_science_and_philosophy

Fingerprint Dive into the research topics of 'Identity in homotopy type theory: Part II, the conceptual and philosophical status of identity in HoTT'. Together they form a unique fingerprint.

Cite this