The n-Category Café

Peter Aczel was the initial advocate of such a thing here, and I think it’s a great idea. Given that computer proof assistants are not really yet sufficiently automated to make formalization of nontrivial arguments palatable to the average mathematician — a situation which I think it will probably take a few decades to overcome, at least — in order for homotopy type theory to make real headway as a foundation for mathematics in the near future, we need a way to do it without computers.

It’s worth noting that the relationship between formal and informal being envisioned here is, to a large extent, backwards from the historical situation for traditional foundations. Traditionally, mathematicians developed our conventions and standards of rigor in natural language by a long, slow process of centuries, and only in the last hundred years or so did people start to write down formal systems in which such reasoning could be codified. By contrast, now we are starting with a formal system — homotopy type theory — and trying to design conventions and standards for a corresponding informal language. The situation isn’t quite as clear-cut as that — in particular, in the 20th century formal systems did also conversely influence the conventions of informal mathematics — but nevertheless I think that this proposal is, by and large, something that’s never been done before.

Another point that I think is very important is that informal HoTT is intended to be read by people who are already familiar with the conventions. Obviously, we don’t want to depart unnecessarily from the language of classical mathematics, but writing informal HoTT is not intended to be the same as writing about HoTT for newcomers to the field, just as we don’t write mathematics in research papers in the same way that we write undergraduate textbooks.

There are a lot of interesting aspects to informal HoTT, and I’ll probably be blogging about them more in the future. However, one of the trickiest and most contentious aspects (unsurprisingly) is the treatment of logic and propositions. Recall that one of the insights of type theory is the propositions as types paradigm, according to which

• Propositions (in the logician’s sense of “assertions which we might attempt to prove”) are identified with particular types, and
• Proofs of a proposition are identified with terms belonging to such a type.

This has all sorts of nice consequences. The common type forming operations, like cartesian product, disjoint union, function types, dependent products, etc. correspond precisely to the usual logical connectives and quantifiers, like “and”, “or”, “implies”, and “for all”. Proofs are endowed with constructive/computational content, which means that sometimes you can automatically extract an algorithm from a proof. It makes for a pleasing parsimony of foundational notions: type theory is all we need, rather than a set of axioms (like set theory) formulated within an external “logic”. And so on.

The slippery question is, which types are the propositions? I wrote about a couple of potential choices back in January: we could allow all types to be propositions, or we could allow only the $(-1)$-truncated types (sometimes called “h-propositions”). This matters because when writing informal type theory, we want to be able to use traditional mathematical phrases like “there exists an $x:A$ such that $P(x)$”, but it seems that the formal meaning of such a phrase must depend on which types we allow to be propositions. If all types can be propositions, then “there exists an $x:A$ such that $P(x)$” can indicate the type $\sum_{x:A} P(x)$, but if only (-1)-types can be propositions, then the same phrase (assuming that it is to be a proposition) must denote instead the (-1)-truncation of $\sum_{x:A} P(x)$ (the bracket type).

In January, I argued strongly for the latter choice (propositions must be (-1)-types). But over the past few weeks, conversations with Bob Harper, Dan Licata, Peter Aczel, and others have brought me around to a different point of view (which nevertheless may not be the same as their point of view…). Consider the following points:

• When doing verified programming, frequently one does want to “prove a theorem” about a program one has written, and then extract computational content from that proof. This is not possible if when one is “proving a theorem” one must always be truncating types. (I don’t personally understand the details of this, so I’m taking their word for it. But even if this were not true, or if you’re a pure mathematician who doesn’t care beans about the needs of computer programmers, I still think the other arguments I’m about to present carry weight.)

• Many of the arguments for h-propositions, when regarded at a formal level, imply only that (-1)-truncated types are important. A priori, they don’t force us to regard such types as the “propositions”; they only force us to talk about them, in some way.

• As I mentioned in my January post, arguably one of the insights of homotopy type theory is that there’s nothing special about (-1)-truncation. (-1)-truncated types are only the first rung on an infinite ladder. At the time, I used this to argue that they shouldn’t be treated specially the way that they are in set theory, where “logic” is an external structure — but insisting that only they should be regarded as the “propositions” is also a form of special treatment.

• Even more generally, truncation levels themselves are not even necessarily that special: they are just particular “higher (idempotent, monadic) modalities”, i.e. stable factorization systems. (I wrote up a brief summary of such modalities from a type-theoretic perspective here.) Arguably, any such modality gives us an equally good “logic”. This includes other useful examples like codiscreteness in a cohesive topos, the double-negation modality for classical logic, and the “local” modalities of subtoposes. It seems likely to me that it would even allow us to handle the logic of strong-subobjects in an $(\infty,1)$-quasitopos, which in January I thought that only logic-enriched-type-theory could handle.

• Finally, in everyday mathematics, not all the “propositions” we prove are naturally (-1)-truncated! Once my eyes were opened to this, I started to see it everywhere. Most classical mathematicians are deeply programmed to think of proofs as containing no content, in the sense that once you prove a theorem it doesn’t matter what the proof was (a type theorist calls this “proof irrelevance”). But actually, in doing ordinary mathematics it happens to me all the time that I end up writing “by the proof of Lemma 9.3”, because what matters is not just the statement of Lemma 9.3 but the particular proof of it that I gave.

  This is especially common for statements such as “$A\cong B$”. In practice, (1) to prove that two things are isomorphic, almost without exception we construct a particular isomorphism, and (2) very often in order to use the fact that two things are isomorphic, we need a particular isomorphism, and it often matters what that isomorphism is. In other words, when we “prove” a statement of the form $A\cong B$, almost always we are not constructing a term in some (-1)-type (which would have to be the (-1)-truncation of the type of isomorphisms from $A$ to $B$), but rather constructing a term in the type of isomorphisms from $A$ to $B$. Therefore, why not allow “$A\cong B$” to denote the type of isomorphisms?

This last point reminds me of Bishop’s comment that the axiom of choice is most often used to extract elements from equivalence classes into which they should never have been put in the first place. If what we have actually constructed is a particular term belonging to some informative type (one that isn’t (-1)-truncated), why force ourselves to say less by asserting only that the (-1)-truncation of that type is inhabited, simply because we want to “prove a theorem” and we dogmatically require that “theorems” must be (-1)-types?

Just as intuitionistic logic is more expressive than classical logic because it doesn’t force us to assume the law of excluded middle (but allows us to assume it as an additional hypothesis like any other hypothesis), type theory is allowing us to see a further distinction which was invisible to the classical mind: we aren’t forced to (-1)-truncate all theorems (but we are allowed to, if we so desire, by simply applying the truncation operator).

(There is another point that seems important too: namely, in homotopy type theory, even the “irrelevant” types — that is, (-1)-types — can be, in a sense, relevant. For instance, the type $isEquiv(f)$ which asserts that $f$ is an equivalence is a (-1)-type, so that any two inhabitants of it are equivalent. However, in proving $isEquiv(f)$ we must supply, among other things, an inverse to $f$, while from an inhabitant of $isEquiv(f)$ we may extract an inverse of $f$, and unless we did something stupid, the inverse we get out is the one we put in — not just equivalent to it, but literally definitionally the same as it. Sometimes this can be really important, especially when implementing things in a proof assistant, because definitional equality controls type-checking — not to speak of computational behavior and efficiency. The other day we had a very interesting discussion about which of the many types equivalent to $isEquiv$ should be used in the HoTT Coq library as “the” definition of equivalence; we eventually settled on “adjoint equivalences” because they specify the most additional data in an easily-extractable form.)

With all the above in mind, I think what I would really like to do is to make a clean break by expunging the notion of “proposition” from the language. In other words, there are only types. Some types are (-1)-truncated. Some types are $n$-truncated. Some types belong to other modalities. Sometimes we can construct a term in a given type as it stands. Other times we can only construct a term in some truncation of it, or in its reflection into some other modality. (For instance, this is quite a common occurrence for the “classical logic” modality.)

Realistically, of course, the word “proposition” is not going to go away. For one thing, it’s a very convenient word to use to describe (-1)-types. But I still believe this way of thinking—freeing ourselves from our percieved need to distinguish between what I called the “two activities” of mathematics, namely “constructing” and “proving”—is the way of the future.

We do still have to choose how to interpret informal statements like “there exists an $x:A$ such that $P(x)$” as types. I think the point that “(-1)-types are not special” argues strongly that (1) such a phrase should, by itself, be interpreted as $\sum_{x:A} P(x)$, but also that (2) there must be an easy and concise way to indicate when we want it to be interpreted in some other modality. And the obvious idea for (2) is to use adverbs, which are a part of speech frequently used to denote modalities (consider the most traditional modalities such as “necessarily” and “possibly”). For instance, we can say “there codiscretely exists …” or “there classically exists …” to indicate application of the $\sharp$ modality or the double-negation modality.

We would, of course, have to choose a particular adverb to indicate the (-1)-truncation modality. One possibility would be “irrelevantly” (referring to “proof irrelevance”), but (aside from being five syllables) that has the quite undesirable implication of “not related to the rest of what I’m saying”. The best adverb I’ve thought of so far is “purely”, as used in classical statements like “this is a pure existence proof, not a construction”. Thus, for instance, we would have the different forms of the axiom of choice:

1. “If for every $x:A$, there exists a $y:B$ such that $P(x,y)$, then there exists a function $f:A\to B$ such that for all $x:A$ we have $P(x,f(x))$” — this one is provable.

2. “If for every $x:A$, there purely exists a $y:B$ such that $P(x,y)$, then there exists a function $f:A\to B$ such that for all $x:A$ we have $P(x,f(x))$” — this one is a strong axiom.

But I’m open to other suggestions. It would also be nice to have an adverb that could be parametrized by a number to denote $n$-truncation. I guess we could say “$n$-purely” for this, though with the unfortunate convention that the unadorned “purely” would imply $n=-1$. On the other hand, thinking semantically, one might also consider “locally”, since (-1)-truncated truth descends along effective epimorphisms. However, this intuition is questionable from a foundational point of view, and probably the adverb “locally” should be reserved for lex modalities, i.e. subtoposes.