Browse/search for people

Publication - Dr Stuart Presnell

    Identity in homotopy type theory, part I

    The justification of path induction

    Citation

    Ladyman, J & Presnell, S, 2015, ‘Identity in homotopy type theory, part I: The justification of path induction’. Philosophia Mathematica, vol 23., pp. 386-406

    Abstract

    Homotopy Type Theory (HoTT) is a proposed new language and foundation for mathematics, combining algebraic topology with logic. An important rule for the treatment of identity in HoTT is path induction, which is commonly explained by appeal to the homotopy interpretation of the theory's types, tokens, and identities as (respectively) spaces, points, and paths. However, if HoTT is to be an autonomous foundation then such an interpretation cannot play a fundamental role. In this paper we give a derivation of path induction, motivated from pre-mathematical considerations, without recourse to homotopy theory.

    Full details in the University publications repository