Universes and Univalence in Homotopy Type Theory

James Ladyman, Stuart Presnell

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

2 Citations (Scopus)
611 Downloads (Pure)


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
Issue number3
Early online date15 Jul 2019
Publication statusPublished - Sept 2019

Structured keywords

  • Centre for Science and Philosophy
  • Centre_for_science_and_philosophy


  • 2010 Mathematics Subject Classification03


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

Cite this