Browse/search for people

Publication - Dr Stuart Presnell

    Identity in homotopy type theory

    Part II, the conceptual and philosophical status of identity in HoTT

    Citation

    Ladyman, J & Presnell, S, 2017, ‘Identity in homotopy type theory: Part II, the conceptual and philosophical status of identity in HoTT’. Philosophia Mathematica, vol 25., pp. 210-245

    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.

    Full details in the University publications repository