Univalent foundations as structuralist foundations (Q1708879)

Univalent foundations (UF), which grew out of homotopy-theoretic models of Martin-Löf type theory, replace sets with homotopy types as fundamental objects. In the paper under review, the author argues that UF may provide a suitable formalisation of the structuralist approach to mathematics. To this aim, he formulates a criterion that a foundation is required to satisfy to be identified as structuralist, namely that, for any branch of mathematics, the expressible properties should be invariant under the relevant criterion of identity. For example, in group theory the properties that our formal system allows us to formulate should be invariant under isomorphism. The author then explains how both Zermelo-Fraenkel set theory and the elementary theory of the category of sets fail to meet this requirement. The more technical part of the paper is devoted to arguing that UF do allow a faithful formalisation of the concept of ``relevant criterion of identity'' under which all well-formed predicates are invariant. The last section discusses and counters three arguments against the role of UF as a foundation for the whole of mathematics (a so-called ``big-f'' foundation).