Universes and Univalence in Homotopy Type Theory

James Ladyman, Stuart Presnell

Research output: Contribution to journalArticle (Academic Journal)

1 Citation (Scopus)
200 Downloads (Pure)

Abstract

The Univalence axiom, due to Vladimir Voevodsky, is often taken to be one of the most important discoveries arising from the Homotopy Type Theory (HoTT) research programme. It is said by Steve Awodey that Univalence embodies mathematical structuralism, and that Univalence may be regarded as 'expanding the notion of identity to that of equivalence'. This article explores the conceptual, foundational and philosophical status of Univalence in Homotopy Type Theory. It extends our Types-as-Concepts interpretation of HoTT to Universes, and offers an account of the Univalence axiom in such terms. We consider Awodey's informal argument that Univalence is motivated by the principle that reasoning should be invariant under isomorphism, and we examine whether an autonomous and rigorous justification along these lines can be given. We consider two problems facing such a justification. First, there is a difference between equivalence and isomorphism and Univalence must be formulated in terms of the former. Second, the argument as presented cannot establish Univalence itself but only a weaker version of it, and must be supplemented by an additional principle. The article argues that the prospects for an autonomous justification of Univalence are promising.

Original languageEnglish
Pages (from-to)426-455
Number of pages30
JournalReview of Symbolic Logic
Volume12
Issue number3
Early online date15 Jul 2019
DOIs
Publication statusPublished - Sep 2019

Keywords

  • 2010 Mathematics Subject Classification03

Fingerprint Dive into the research topics of 'Universes and Univalence in Homotopy Type Theory'. Together they form a unique fingerprint.

  • Cite this