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 B, were both involved in the process of publication of the article 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. A thought that the consistent
use of formulas like
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 B‘s interest in logic is limited. My understanding is that A 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.
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  and , 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.