Homotopy Type Theory

Out in the strange world beyond the pseudonyms (or, actually, the realm of different pseudonyms, used by other people) there is noise surrounding a new book, a collaborative work, titled Homotopy Type Theory, to which I can (quite unreliably and unverifiably) claim to have made at least a moral contribution (and one blog post contribution --- no, I'm not telling you here!). And I don't at all mind that my name appears nowhere in the text, because really this sort of thing is more about the fun than the credit (also, two or four dozen other people made much-more substantial-and-original contributions anyway).

The text is subtitled “Univalent Foundations of Mathematics”, which is really a much more interesting notion than “homotopy type theory” as such, and it is about this Univalence that I'd like to sing for just a little while.

Now, for a long time, mathematicians of a certain kind have been competing with eachother to compose a sort of abstract semantics which might conceivably give an underlying meaning to all the abstract nonsense ordinary mathematicians do for a living. This might sound like a funny thing to worry about, but it's had immensely practical results in the realm of computer science and such, whether the dear fellows and dames intended it or not. It also might sound like chasing one's tail (indeed this is a danger that competitors of the sport learn early on to avoid), which is probably why Foundations is so emphasized in the name of the specialization.

Anyways, lots of people have composed such schemes of abstract semantics, and so modern mathematicians have lots of variety to choose from whenever they worry about if they're spouting absolute nonsense or merely incomprensible sense; and these do have some interesting distinctions among them — the best foundations are perfectly able to talk about all of the other foundations, and find some interesting things the other foundations say, and explain why they are all wrong. This is part of the sport, you see. Great fun! What settles a mathematician on one foundation or another (some never do settle!) involves a combination of aesthetics, pragmatics, and intuition.

Homotopy Type Theory is, roughly, a language for discussing (and perhaps describing) objects made of stuffs that are put together, somehow. This sounds vague, I know; but it isn't that the words “objects”, “stuffs” or “put together” are intrinsically vague, it's that the rules for using them haven't been made explicit here. They aren't the usual words (except “objects” might be!) but that's immaterial. But there are words, and rules, and the rules let you do enough that one can call the result a language, and even think it versatile; and that's half of what one has come to expect of a foundation these days. The other third and the final quarter are, respectively, some assumptions about what you can assert without comment, and how you decide what follows from which assumptions. (If you're worried that ½ + ⅓ + ¼ is ¹³⁄₁₂, you're paying too much attention).

The Univalence Hypothesis belongs to the third part, assumptions to be quoted without comment, and specifically makes assumptions about some particular objects one can mention, and specific details about how they are put together. In just a little more specificity, it supposes there to be a family of particular objects, called $\mathrm{Type}_j$, that the stuffs each $\mathrm{Type}_j$ are made of are themselves objects, and that every object is party to most of them, and (most importantly) each $\mathrm{Type}_j$ is put together in such a way that equivalence of objects-as-stuffs-put-together is equivalent to objects as parts of $\mathrm{Type}_j$.

That's still vague, because I still haven't written here what the things mean, nor do I intend to, but an illustration might help.

Suppose a pair of twins shared a pair of identical bicycles. Now, the twins know eachother apart from themselves, and the bicycles certainly aren't in the same place, but in our imagination “identical bicycles” really does mean the twins can't distinguish the bicycles by sight, and because they're good detached Catholics they also have no inclination to fight over who is on which bike, and so There Are Two Ways for twins to mount and ride their bikes. The left-hand supposition of Univalence (and our experience in the world of the senses!) is that there is a path, or choreography between these two configurations: twin first-to-breathe and twin first-to-say-“ma!” (if this lists them all two) can dismount and walk around and effectively trade places. The right-hand supposition of Univalence is that there is, effectively, exactly one way to do this and one way to not; and this is where Univalence and the world of sense part ways, because there is no way to exhibit such a simple figure in our paltry three-space-less-one-time dimensions. But the key idea — having exactly one way to switch and one way to not-switch — generalizes in a beautiful and poetic way, and leads to all sorts of other beautiful and poetic equivalences, to say nothing of many subtler rhymes it gives rise to. For instance (one of my favourites!), there is a circle of ways to be the order of the integers. This notion of equivalence, identified with “identifiability”, is the key novelty proposed in Univalent Foundations, is the organizing principle of the book, and makes for some fun thought exercises too.

There's lots lots more (of course! we'll never be finished) and this wasn't ever meant to be a math 'blog, however fun maths is; so I'll leave off there, and if you want to go read more about it elsewhere, perhaps we'll meet again by other names and in other guise.

à bien-tôt!