Skip to content

Universes and Univalence in Homotopy Type Theory

Research output: Contribution to journalArticle

Original languageEnglish
Pages (from-to)426-455
Number of pages30
JournalReview of Symbolic Logic
Issue number3
Early online date15 Jul 2019
DateAccepted/In press - 8 Dec 2016
DateE-pub ahead of print - 15 Jul 2019
DatePublished (current) - 1 Sep 2019


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.

    Research areas

  • 2010 Mathematics Subject Classification03

Download statistics

No data available



  • Full-text PDF (accepted author manuscript)

    Rights statement: This is the accepted author manuscript (AAM). The final published version (version of record) is available online via Cambridge University Press at . Please refer to any applicable terms of use of the publisher.

    Accepted author manuscript, 361 KB, PDF document

    Licence: Other


View research connections

Related faculties, schools or groups