Are Univalent Foundations of mathematics a modern version of logicism?

Question

As I understand it (and mine is just basic understanding) the Univalent Foundations program is an attempt to reduce mathematics to an interpretation of Martin-Löf type theory by using homotopy theory. Is this not a revamped version of the logicist program (using type theory instead of FOL and homotopy theory as the semantics) and, consequently, doesn't it face the objections logicism faced? By the logicist program I mean the (Fregean) attempt of reducing mathematics to logic.

Answer 1

If anything, univalent foundations share more with constructivism and formalism than with logicism, and even with them it shares technical apparatus more than motivations. Logicism was an ambitious project to ground all of mathematics in the self-evident laws of thought. Russell's paradox brought the realization that "laws of thought" were not as self-evident as they seemed, and Principia demonstrated that devices needed to avoid paradoxes and recover all of mathematics (like types and reducibility) are contrived and go beyond any plausible conception of logic. On the other hand, Wittgenstein's Tractatus showed what is forthcoming from plausibly logical means, iteration and substitution. That would be primitive recursive arithmetic, not even all of arithmetic, let alone all of mathematics. The last version of logicism, relativized to "linguistic frameworks" by Carnap, had a great deal of Hilbert's formalism mixed in, and was undermined along with it by Gödel's results.

Univalent programme, a.k.a. homotopy type theory (HoTT), is very young (key ideas emerged in 2005-2014) and far more pragmatic, The name "univalent" is meant in the sense of "faithful":

"Voevodsky explained his choice of the term “univalent” in [62]: it comes from a Russian translation of the Boardman and Vogt's book Homotopy Ivariant Algebraic Structures on Topological Spaces, here the term “faithful functor” is translated as “univalent functor”. He also said, “Indeed these foundations seem to be faithful to the way in which I think about mathematical objects in my head.”"

The idea is not to give mathematics a new philosophical justification, but to reconstruct most of it from a new point of view that is particularly friendly to constructive methods and automated proof verification.

"Part of the reason that Martin-Löf type theory employed in the univalent setting is that this theory has good computational properties. In technical terms, type checking in this theory is decidable. Consequently, it is possible to implement the theory on a computer. This is essentially what has been done in the case of the proof assistants Coq and Agda."

Other exciting features are that the new model of type theory (constructivist logic) found by Voevodsky in 2009 naturally interprets some of its "oddities", and is unexpectedly and non-trivially connected to more traditional areas of mathematics. Logic is modeled using topological notions, specifically homotopy theory, e.g. identity is treated as a homotopy equivalence. This allows to formalize in a principled way one of mathematicians' favorite tricks, identifying isomorphic structures. Which in turn links univalent foundations to the category theory, also well known for its intuitionistic models (elementary topoi), but with a richer and more flexible structure.

However, there is no contention that types and homotopy are more fundamental than sets, categories or other mathematical notions. Univalent foundations are meant to be a particular mathematical theory, albeit widely applicable, one foundation among many, geared to a pragmatic purpose (proof checking in Coq is even likened to typing in Latex). In this sense it is like one of Carnap's "linguistic frameworks", but without Fregean or Hilbertian ambitions.

For a brief survey I recommend first two sections of Pelayo-Warren's Homotopy Type Theory and Voevodsky's Univalent Foundations, which are more lucid than Wikipedia's articles on both subjects. The most recent review is Grayson's Introduction to univalent foundations for mathematicians.