This morning I had breakfast at the n-category café and was pleased to see that Mike Shulman had posted a draft of his chapter on Homotopy Type Theory and Univalent Foundations (HOTT/UF) for a book called Categories for the Working Philosopher, edited by Elaine Landry of UC Davis. I have been trying for several years to grasp the meaning of Voevodsky’s univalence axiom, and Shulman’s earlier explanations were as comprehensible as anything I had seen, but the meaning kept slipping away every time I turned my attention to something else (like number theory). Shulman’s draft has an explanation for that as well:
we should beware of judging a theory to be more intuitive or fundamental merely because we are familiar with it: intuition is not fixed, but can be (and is) trained and developed. At present, most mathematicians think of ∞-groupoids in terms of sets because they learned about sets early in their mathematical education; but even in its short existence the HOTT/UF community has already observed that graduate students who are “brought up” thinking in HOTT/UF form a direct understanding and intuition for it that sometimes outstrips that of those who “came to it late.”
Shulman’s new draft is as clear as one could wish, but I still can’t stay focused on the special role of univalence. It may just be that I don’t care enough. Shulman writes
over the past few decades ∞-groupoids have come to play a more and more central role in mathematics and even physics, starting from algebraic topology and metastasizing outwards into commutative algebra, algebraic geometry, differential geometry, gauge field theory, computer science, logic, and even combinatorics.
Note that number theory is not on that list; nor are geometric analysis, Fourier analysis, dynamical systems, or PDEs. I think this is no accident, but the reasons I am tempted to give don’t really stand up to scrutiny, so I’ll just leave it at that. As a matter of fact, though, ∞-groupoids have been creeping closer — “metastasizing” would be an ominous way of putting it — to number theory, by way of the geometric Langlands program. Increasingly I hear my colleagues confess to have been sneaking looks at Lurie’s Higher Topos Theory — at least the first chapter, which, according to some geometric Langlands specialists, contains everything we really need. (I note in passing that none of the chapters of Landry’s book is devoted to the philosophical significance of the use of categories by Grothendieck, much less to Lurie’s more recent work, and I find this surprising.) But none of the number theorists I know seems to feel an urgent need for new foundations — I should write Foundations, because the new (lower case f) foundations of p-adic geometry being developed by Peter Scholze and his collaborators are seen by many, at least retrospectively, as long overdue. I suspect this comment on Shulman’s post is the reason:
the driving force behind HoTT/UF as a foundation is not necessarily for it to become the “ultimate” foundation e.g. like ZFC. The driving force, rather, is to provide foundations formalizable in a proof assistant so that the use of proof-assistants can actually become a tool for working mathematicians. From this perspective it is clearly preferable to rely on a formal system that was tailor-made to be implemented in computers.
I don’t know of anyone in my branch of number theory who especially wants this kind of tool.
I once met Mike Shulman and was hoping to ask him to explain the univalence axiom, but long before we reached that point he stumped me by claiming that I was taking “set” as a primitive notion subject to axioms and that I should be able to do the same with “type.” Now that I’ve had some time to think about it, I’m sure I disagree, because I didn’t actually learn the ZFC axioms until I had been a mathematician for many years. So I must have picked up a non-axiomatic way of working with sets. As I write in the book,
The [mathematical] socialization outlined in chapter 2 had less to do with assimilating norms, values, and respect for a transhistorical hierarchy than with learning to use the word “exist” appropriately and effortlessly, to display a pragmatic “belief in” the world of mathematical objects adequate for seamless interaction with the community.
The HOTT/UF community is not pragmatist. I would call them militant enthusiasts. The militancy would explain their insistence on using the unwieldy and unfamiliar notation a:A for “a is an element of [the type] A” rather than the set-theoretic notation a ∈ A, presumably to help overcome the habit of “thinking in terms of sets.” Enthusiasm (and pantheism) are more complicated and are postponed to Part 2.