Mike Shulman has kept the promise he made a few weeks ago by writing a post on the n-category café speculating on the reasons HoTT, as a proposed foundation for mathematics, is in practice closely associated to computer formalization, even though there is no necessary connection

between the two.

Shulman’s post is comprehensive; he does his best to cover all the angles and he invites readers to let him know if he has missed anything. It clears up some misconceptions (including mine) and should be read as a background to the online articles mentioned in this post. It all makes sense, and I don’t really have anything to add, but since I already have your attention, I may as well share something I learned from two colleagues during the past few weeks. The two colleagues, whom I will call * A* and

*, were both involved in the process of publication of the article*

**B***Homotopy type theory and Voevodsky’s univalent*

*foundations*, by A. Pelayo and M. A. Warren, which appeared last October in the

*Bulletin of the American Mathematical Society*.

*thought that the consistent*

**A**use of formulas like

and

would discourage mathematicians from reading the article, and suggested that they be rewritten in more familiar (set-theoretic) notation. * B*, on the other hand, found it perfectly natural that the authors would use the notation to which they are accustomed, and didn’t see why mathematicians who are not practiced in logic or programming would have any trouble adapting.

As it happens, * A* has extensive experience with type theory whereas

*‘s interest in logic is limited. My understanding is that*

**B***felt that the authors did themselves a disservice by limiting their audience to those familiar with their notation. I have to agree. I’ve just discovered that Section 2.3 of the Pelayo-Warren article contains a statement of the univalent axiom that I almost understand. Maybe there are others, but I haven’t seen them. The section begins comprehensibly with a discussion of homotopy types that doesn’t mention type types. But I assume I have to be able to read the formulas above in order to appreciate the fact that the category of simplicial sets provides a model of type theory in which the univalent axiom holds. And it is likely that, after I spend the time learning to read the notation, I will come to the conclusion that this fact doesn’t matter to me very much.*

**A**Pelayo and Warren mention this in the introduction:

Although interesting in its own right, this perspective becomes significantly more notable in light of the good computational properties of the kind of type theory employed here. In particular, type theory forms the underlying theoretical frame- work of several computer proof assistants such as Agda and Coq (see [18] and [9], respectively), and these can be used to formalize mathematics done in the univalent setting.

The judgment “significantly more notable” does not mesh naturally with Shulman’s post. It’s not clear to me whether or not Shulman and the authors of the *Bulletin* article see matters the same way.

David RobertsFor the benefit of readers who find type notation completely mystifying, I can unpack that first one, in a very rough and ready way.

A colon (:) is very similar to ‘element of’ (\in, in LaTeX). One can ignore the differences for a first pass. The turnstile (|-) means something like ‘given the LHS, one has the RHS’.

In this context (pun not intended), in the top line we have for each x in B, an element s(x) in E(x), where E is a family of types (spaces, whatever) parameterised by points in B.

The bottom line gives an element in the product over all of the family, labelled by the lambda term. When you think about what this is, it is a section of the map E -> B (compare to the two formalisations of the axiom of choice: products are non-empty vs a section of a surjection).

The horizontal line means given the top, you get the bottom (this is different to the turnstile for important reasons, not important for first run). Thus given a family of types, each with some element, one gets an element of the product over the family.

LikeLike

Mike ShulmanOne of the fun things about the HoTT/UF community is its diversity, not just of backgrounds but of viewpoints. Having said that, I don’t think I see anything I disagree with in the paragraph you quoted from Pelayo-Warren; I did say in my post that “many of us believe that HoTT is actually the best formal system extant for computer formalization of mathematics,” which I would say qualifies as making it significantly more notable. I can’t say, of course, whether they would agree with everything I’ve said.

Regarding the question of notation, I’m also basically in

‘s camp. Outside of a short appendix, we deliberately omitted all those horizontal lines and turnstiles (the “⊢” symbol) when writing the HoTT Book. (I do, however, insist on using colons for typing judgments rather than set-membership, x:A rather than x∈A. I think using the latter creates more confusion than it solves, because the two are really quite different things.)AI would venture to suggest that

‘s background means his/her opinion was the more informed of the two; perhaps he/she had some experience trying to explain type theory to non-type-theorists, or even remembered his/her own experience learning type theory for the first time. My own experience with those two things suggests that this sort of notation should be avoided like the plague until the reader is “sold” on type theory (and maybe even then).A‘s position (“perfectly natural that the authors would use the notation to which they are accustomed”) is certainly understandable, and in most areas of mathematics I would probably agree, as long as the notation is introduced carefully before use (in a paper intended for a wider audience). But I think the notation in type theory is unusually difficult for outsiders to grok. This is partly because type theory is fundamentally aBtheory about syntax, so it’s natural that syntax plays a more central role than mathematicians are used to. But there’s more to it than that: the notation of type theory also seems to “play by different rules”. E.g. to a mathematician off the street, the order of operations may not even be clear; can you tell at a glance that “x:A,y:B⊢c:C” should be parsed as “((x:A),(y:B))⊢(c:C)” and not as “(x):(A,y):(B⊢c):C”, especially given that TeX puts more space around colons than around commas by default? I don’t really have a good guess as towhytype-theoretic notation is so different and difficult, though.LikeLiked by 1 person

mathematicswithoutapologiesPost authorBoth

andAare very distinguished mathematicians; you are right thatBhas had a great deal of experience explaining unfamiliar ideas from logic and computer science to audiences of pure mathematicians, and is considered extremely effective at doing that. It would be convenient for me to believe that the reason the ideas are so hard to get across is the one you pointed out: “type theory [like other theories derived from formal logic] is fundamentally aAtheory about syntax, so it’s natural that syntax plays a more central role than mathematicians are used to.” If I believed in “natural kinds,” I would even speculate that computer scientists, logicians, mathematicians, and physicists, are distinct natural kinds, and their differences can be detected by the facility with which they adapt to the characteristic forms of expression, or intuition, of the respective categories. I could continue and speculate that whether one will turn out to be a number theorist or a homotopy theorist (for example) is embedded in one’s neurons, or family history, or reflects a genetic predisposition… I won’t go so far as that, but I do agree with the Donaldson quotation from an earlier post that mathematical intuition is about something other than syntax, and I haven’t yet given up hope that philosophers will help figure out what that is without resorting to vacuous allusions to social convention.Some lucky individuals are able to develop facility with more than one of these forms of expression. I am not one of them, so while I am grateful to David Roberts for his explication of the symbols in the displayed formulas, I can only hope that they will be of use to other readers.

I wanted to add a comment on the fifth point in your n-Cat post, the one about sociology and Voevodsky’s central role in associating HoTT with computer formalization. I am very sensitive to this “charismatic” phenomenon for a reason I have hardly had an opportunity to discuss: the difficulty in escaping the model of history of mathematics as the history of discoveries by great individuals (usually great men). This is reflected in the expectations of publishers: since it’s so hard to explain mathematics to a general audience, a popular book that is not about a universally available concept (like zero or infinity) almost always has to follow a quest narrative, with a heroic figure at the center. I wanted my book to reflect experience at the level of the mathematical community; however, I note that at this very moment, it ranks #2212 on the Canadian Amazon site in the category of memoirs (in the past it was much higher), although by no stretch of the imagination can it be considered a memoir! Publishers must also be a natural kind. (Princeton University Press, to their credit, did not impose this model.)

LikeLiked by 1 person

Mike ShulmanI agree that the intuition in most mathematics is about something other than syntax. But, of course, when the mathematics we are doing is

aboutsyntax, the relevant intuitions will also be about syntax. On its own, though, I don’t think this can explain why type theory is more difficult for outsiders, since in any field of mathematics the intuitions will be about something peculiar to that field.My reaction to the Donaldson and Atiyah quotes mentioned in the previous post is somewhat different from yours. Take Atiyah’s quote for instance: “I may think I understand, but the proof is the check that I have understood.” I presume his point and yours is that proof isn’t what mathematicians spend most of their time

thinkingabout when doing mathematics. I’m not sure whether or not I agree with that based on my own experience, but laying it aside for the moment, he still concedes that the proof is anarbiter of correctness: if the proof doesn’t work out, then there’s something we haven’t yet understood. I think that’s a strong argument that whether or not proof is central to the thought processes of mathematicians most of the time, it is nevertheless still thesine qua nonof mathematics.LikeLike

mathematicswithoutapologiesPost authorI don’t think we disagree about anything, but we seem to be drawing different conclusions. I can’t put my finger on the difference; all that comes to mind is a cryptic observation, namely: Frege saw Cantor’s set theory and established the bases of modern symbolic logic; the Nietzschean Hausdorff saw Cantor’s set theory and (with the help of some Russian name-worshippers) established the bases of modern topology. This last was one of my big surprises when I wrote the book.

LikeLike