Identity in homotopy type theory, part I: The justification of path induction

James Ladyman, Stuart Presnell

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

18 Citations (Scopus)

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.

Original languageEnglish
Article numbernkv014
Pages (from-to)386-406
Number of pages21
JournalPhilosophia Mathematica
Volume23
Issue number3
DOIs
Publication statusPublished - 1 Oct 2015

Research Groups and Themes

  • Centre for Science and Philosophy
  • Centre_for_science_and_philosophy

Fingerprint

Dive into the research topics of 'Identity in homotopy type theory, part I: The justification of path induction'. Together they form a unique fingerprint.

Cite this