Browse/search for people

Publication - Professor James Ladyman

    Universes and Univalence in Homotopy Type Theory


    Ladyman, J & Presnell, S, 2016, ‘Universes and Univalence in Homotopy Type Theory’. Review of Symbolic Logic.


    The Univalence axiom, due to Vladimir Voevodsky, is often taken to be one of the most important new 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’. In this paper we explore the conceptual, foundational and philosophical status of Univalence in Homotopy Type Theory. We extend our Types-as-Concepts interpretation of HoTT to Universes, and offer 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 justifi-
    cation 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 paper argues that the prospects for an autonomous justification are promising.

    Full details in the University publications repository