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 language | English |
---|---|
Pages (from-to) | 210-245 |
Number of pages | 36 |
Journal | Philosophia Mathematica |
Volume | 25 |
Issue number | 2 |
Early online date | 15 Dec 2016 |
DOIs | |
Publication status | Published - 1 Jun 2017 |
Research Groups and Themes
- Centre for Science and Philosophy
- Centre_for_science_and_philosophy