The n-Category Café

From a foundational point of view, what we’re doing today is analogous to developing mathematics in set theory. When you learn ZFC, you learn to define (for instance) Kuratowski ordered pairs, cartesian products, functions as sets of ordered pairs, and so on, eventually building up all the familiar structures of mathematics. Similarly, starting from homotopy type theory, we need to do some building up of familiar concepts, although of course the process will be different since we have different starting notions.

I’m mostly going to describe this informally, avoiding the formal syntax of type theory with its turnstiles, judgements, and derivations. And I’m not going to make any use of the correspondence we talked about last time, but there is one advantage to having described that correspondence first: namely, if it makes you more comfortable, you can think of everything I say today as a description of constructions performed in a category with a nicely-behaved WFS. You can even (and, in fact, should) think of topological spaces or simplicial sets with their usual (acyclic cofibration, fibration) WFS (although there are technical issues involved in making that precise, which are discussed in the references I linked to last time).

Now, where do we start developing mathematics? What we have is a basic notion of homotopy type (a.k.a. $\infty$-groupoid), including dependent types, identity (or “path”) types, dependent sums and products, and perhaps some other constructors (like inductive and coinductive types). This is great for doing homotopy theory, but in a lot of mathematics there is not (yet) visible any homotopical behavior; thus we really need also a notion of “set” to be a good foundational system.

Classically, sets can be identified with homotopy types that are discrete: they contain no nonidentity morphisms/paths/homotopies (or higher such). That notion isn’t invariant under equivalence, but there is a corresponding notion which is: we require instead that the space of paths/morphisms between any two points is either empty or contractible. (If it is contractible, then the two points represent the “same element” of the corresponding set.) I’m going to follow the homotopy theorists and call types of this form homotopy 0-types, or 0-types for short.

Of course, we should also have a notion of homotopy $n$-type (a.k.a. $n$-groupoid) for all natural numbers $n$. We can define these inductively by saying that the space of paths between any two points in an $n$-type should be an $(n-1)$-type. And, as regular $n$-Café readers will know, we can continue downwards a couple of steps: the inductive definition gives the right answer for $n=0$ if a “(-1)-type” is one which is either empty or contractible, which is equivalent to saying that the space of paths between any two points in it is contractible. And the inductive definition then gives the right answer for $n=-1$ if a “(-2)-type” is one which is contractible. Cf. negative thinking.

(By the way, Voevodsky says a type is of h-level $(n+2)$ where I would say it is an $n$-type. This has the benefit of starting the numbering at $0$ rather than $-2$, but it has the disadvantage of not matching the well-known numbering of homotopy types and groupoids. Use whichever you prefer.)

Thus, in order to define $n$-types inductively for all $n$, we just need to get things started at $n=-2$ by defining when a type is “contractible.” However, before we do that, we need to address a different issue, which may be one of the trickiest aspects of homotopy type theory for a non-type-theorist to get used to.

We’ve said that we expect to recover set theory from 0-types, groupoid theory from 1-types, and so on. But that means we should also expect to recover logic from $(-1)$-types. (The empty type represents “false,” while the contractible one represents “true”—and in intuitionistic logic, there can be more $(-1)$-types than that.) In particular, we should not include an external “logic” in our foundational theory. Statements such as “$X$ is a 0-type” or “$Y$ is contractible” should not be things we say about the theory which can be true or false; rather they should be (-1)-types themselves. The “truth” or “falsity” of such a proposition then corresponds to whether or not we can exhibit a point of the corresponding (-1)-type.

It may seem like we’ve painted ourselves into a bit of a corner here: we need to define what it means to be a (-1)-type, as part of our inductive definition of $n$-types for all $n$, but that “definition” must itself be a (-1)-type. However, if we sit back calmly and think about it, we can see there isn’t really a problem. All we need to do is define, for any type $X$, a type $IsContr(X)$ representing the proposition “$X$ is contractible,” such that when we then go on to define “$X$ is a (-1)-type” in terms of “$X$ is contractible,” the type $IsContr(X)$ turns out to in fact be a (-1)-type. It’s a bit bootstrappy, but not circular or paradoxical.

So how do we define $IsContr(X)$, in such a way that it is always either empty or contractible? A natural idea, if we should happen to think of it, is that we should define $IsContr(X)$ to be the type of contractions of $X$. This is logical because if a space $X$ is contractible, then its space of contractions is itself contractible, while if $X$ is not contractible, then its space of contractions is of course empty. We formalize this as follows:

$$IsContr(X) \coloneqq \Sigma_{x\in X} \Pi_{y\in X} Paths_X(x,y)$$

I’m writing $Paths_X(x,y)$ for the identity type of $X$ (what was previously written $Id_X(x,y)$), since in homotopy type theory we interpret it as a type of paths, or equivalences, rather than equalities. If we unpack the above definition, we see that a point of $IsContr(X)$ consists of a point $x\in X$ together with, for every $y\in X$, a path from $x$ to $y$. The point $x$ is the “basepoint” or “center” to which we are contracting, and the paths supply the “contraction.” Remember that all constructions on types are “natural” or “continuous,” so that the selection of paths is necessarily natural/continuous in $y$, as we should require.

The above definition of $IsContr(X)$, due to Voevodsky (like pretty much everything else we’re doing today), is a bedrock on which the rest of the edifice rests. I’ve tried to make it seem inevitable in hindsight, but I certainly don’t think I could have come up with it myself!

Voevodsky then proved the following theorem:

$$IsContr(X) \to IsContr(IsContr(X))$$

Now actually, like everything else in type theory, $IsContr(X) \to IsContr(IsContr(X))$ is a type: the type of functions from $IsContr(X)$ to $IsContr(IsContr(X))$. So when I say he “proved” it, I mean that he exhibited, by formal type-theoretic constructions, a specified point of that type: a function from $IsContr(X)$ to $IsContr(IsContr(X))$. Once we define (-1)-types, we can show that $IsContr(X) \to IsContr(IsContr(X))$ is actually a (-1)-type, so that it contains at most one point; hence exhibiting a point of it is sufficient to show that it is “true,” which is what we mean in general by “proving a theorem.”

So what does this theorem mean? The type of functions between two propositions is just an implication, so this theorem means that if $X$ is contractible, then so is $IsContr(X)$: the space of contractions of a contractible space is contractible. On the other hand, if $X$ is not contractible, then $IsContr(X)$ is empty, since a point of $IsContr(X)$ would be a contraction of $X$. Thus $IsContr(X)$ is, at least intuitively, a (-1)-type, as desired.

There’s a slight subtlety here, though: we almost certainly can’t prove this theorem in plain unmodified intensional type theory. This is because $IsContr(X)$ contains, among other things, a (dependent) function type, and so $IsContr(IsContr(X))$ contains, among other things, the path (identity) type of a function type—but fully intensional type theory does not specify what the identity types of function types are like. In particular, it can be the case there that two functions are pointwise equal everywhere—i.e. the type $\Pi_{x\in X} Id_Y(f(x), g(x))$ is inhabited—but not themselves equal—i.e. the type $Id_{X\to Y}(f,g)$ is not inhabited. However, for homotopy type theory, we expect a path from $f$ to $g$ to consist exactly of a natural/continuous family of paths from $f(x)$ to $g(x)$, so that these two types should actually be equivalent. Thus we need to augment intensional type theory by an axiom called functional extensionality which asserts this—or else a stronger axiom which implies functional extensionality. I’ll come back to this in the next post.

Before we go on, I want to address a point that’s confused several people, including myself. (If this paragraph confuses you rather than clarifying anything, just skip it.) I described above the homotopical interpretation of $IsContr(X)$: a point of $IsContr(X)$ is a point of $X$ together with a continuous deformation retraction to that point. On the other hand, we can interpret the same definition from a propositions as types point of view, in which the identity type represents equality, $\Sigma$ represents “there exists,” and $\Pi$ represents “for all.” In this case, $IsContr(X)$ translates to “there exists a point $x\in X$ such that all other points $y\in X$ are equal to $x$.” This is a perfectly good notion of what it means for a set to be “contractible”. The mistake is to start thinking of identity types as representing paths, but to keep trying to interpret $\Sigma$ and $\Pi$ as logical quantifiers, forgetting that for consistency with $Path_X$, they must also be interpreted as continuous or natural operations. This mismatched interpretation leads to the conclusion that $IsContr(X)$ means “there exists a point $x\in X$ such that every point $y\in X$ is connected to $x$ by a path”, which sounds like a definition of connectedness, not contractibility.

Okay, let’s go back to our in-progress inductive definition of $n$-types. We’ve defined what it means to be contractible, i.e. to be a (-2)-type. Now we can define “$X$ is a (-1)-type”, a.k.a. “$X$ is a proposition”, as follows:

$$IsProp(X) \coloneqq \Pi_{x,y\in X} IsContr(Paths_X(x,y))$$

This is almost a translation of our proposed definition from above: we wanted to say that $X$ is a (-1)-type if the space of paths between any two points of $X$ is contractible. However, instead of merely asserting that each path space is contractible, giving a point of $IsProp(X)$ specifies a contraction of each path space. In fact, we don’t have any tools yet to construct types which assert that things exist without specifying them—but since the theorem above shows that contractions are unique when they exist, we can hope that the extra data in $IsProp(X)$ will be redundant.

And indeed, Vladimir goes on to prove the following theorems:

$$IsProp(IsContr(X))$$

$$IsProp(IsProp(X))$$

So our bootstrap process is working: we’ve defined the notions of a type “being contractible” and “being a proposition” as types, which are themselves in fact propositions ((-1)-types). Now we can go on:

$$IsSet(X) \coloneqq \Pi_{x,y\in X} IsProp(Paths_X(x,y))$$

and inductively:

$$IsNType(X,n+1) \coloneqq Pi_{x,y\in X} IsNType(Paths_X(x,y),n)$$

Now that we have these definitions, we can hope to prove that sets behave the way we expect sets to, and so on. For instance, the category of sets ought to be an elementary topos. However, all we can prove so far is that it is locally cartesian closed. We can remedy this by assuming, as an additional axiom, that we have a type of all propositions. This will give us a subobject classifier in the category of sets, which will therefore be an elementary topos. (Vladimir calls this a resizing axiom, for reasons that I’ll explain in the next post.)

With a type of all propositions, we can also construct familiar logical operations on (-1)-types, just as we can for subobjects in any topos. I’m talking about connectives like “and” and “or” and quantifiers like “there exists” and “for all”. Of course, since our propositions are (particular) types, we already have the type-theoretic operations like $\times$, $\Sigma$, and $\Pi$, and these sometimes do what we want, but not always—the issue is that they don’t necessarily preserve the property of being a (-1)-type.

For instance, one can prove that if $X$ and $Y$ are (-1)-types, then so are $X\times Y$ (which we therefore call “$X$ and $Y$”) and the function type $X\to Y$ (which we call “$X$ implies $Y$”). Similarly, if $X$ is any type at all and $Y(x)$ is a (-1)-type dependent on $X$, then $\Pi_{x\in X} Y(x)$ is a (-1)-type (which we call “for all $x\in X$, $Y(x)$”). On the other hand, under the same hypotheses $\Sigma_{x\in X} Y(x)$ need not be a (-1)-type; rather than the proposition “there exists an $x\in X$ such that $Y(x)$” it is the type “$\{ x\in X | Y(x) \}$”. What we need is a way of “squashing” any type $Z$ down to a (-1)-type which is inhabited just when $Z$ is. From a homotopy perspective, is natural to call this “squashed” type $\pi_{-1}(Z)$.

There are several ways to obtain this squashing operation. We can assert it as part of the structure of the type theory, as in this paper by Steve Awodey and Andrej Bauer; there $\pi_{-1}(X)$ is written as $[X]$. We can hope to obtain it as a consequence of a general “quotienting” or “exactness” axiom, whose structure is currently unclear, but which I may talk a bit about later on. But we can also derive it from a subobject classifier, in the same way that we prove that any elementary topos is a regular category:

$$\pi_{-1}(Z) \coloneqq \Pi_{P\in \Omega} (Z\to P)$$

where $\Omega$ is the subobject classifier (the type of all propositions).

Thus, intensional type theory with functional extensionality and a subobject classifier seems to be a pretty good foundational system: at least, we can derive familiar-looking theories of logic and sets. Let me finish today by describing another one of Voevodsky’s insights: the definition of when a map is an equivalence. Homotopically, it’s natural to define $f\colon X\to Y$ to be an equivalence if we have a map $g\colon Y\to X$ and paths $p\in Paths_{X\to X}(g f, id_X)$ and $q\in Paths_{Y\to Y}(f g, id_Y)$. This might lead us to the definition

$$?? \qquad IsEquiv(f) \coloneqq \Sigma_{g\colon Y\to X} \; (Paths_{X\to X}(g f, id_X) \; \times \; Paths_{Y\to Y}(f g, id_Y)) \qquad ??$$

but unfortunately this definition does not give us a (-1)-type. We could squash it down to a (-1)-type with $\pi_{-1}$, but it’d be nice to be able to talk about equivalences without needing the axioms that give us $\pi_{-1}$. Voevodsky’s idea was to make use of the fact that $IsContr$ is a (-1)-type, and define $f\colon X\to Y$ to be a weak equivalence if all its (homotopy) fibers are contractible:

$$IsEquiv(f) \coloneqq \Pi_{y\in Y} IsContr( \Sigma_{x\in X} Paths_Y(f(x),y))$$

Here $\Sigma_{x\in X} Paths_Y(f(x),y)$ is the (homotopy) fiber of $f$ over $y$: a point of it is a point $x\in X$ equipped with a path from $f(x)$ to $y$. He was then able to prove:

$$IsProp(IsEquiv(f)).$$

There’s also another way to define $IsEquiv$ that also gives a (-1)-type. Recall that any equivalence of categories can be improved to an adjoint equivalence, but we need to change one of the natural isomorphisms. In fact, given the two functors and one of the natural isomorphism, there is a unique choice of the second one such that the triangle identities hold. However, given just the two functors (assuming they are known to be inverse equivalences), the choice of the two natural isomorphisms is not unique.

This suggests that we need to add more “adjointness” data to make the first definition $IsEquiv$ into a (-1)-type. The first thing we may think of is to add all the higher data going all the way up, to make it a “fully coherent” $\infty$-equivalence. This “would work,” but it is not expressible in the type theory (at least, not easily). However, it turns out that if we cut off at any finite level with “half” of the data at that level, then we still get a (-1)-type. So, for instance, it suffices to specify, in addition to $f$, $g$, $p$, and $q$, a secondary homotopy asserting that $p$ and $q$ satisfy one of the triangle identities. There will then be a contractible space of choices of all the higher data. (It would also work to specify only $f$, $g$, and $p$, except for the fact that given only that data we can’t necessarily conclude that $f$ is an equivalence; $q$ might not exist at all.)

To get some homotopical intuition for why this works, think of constructing $S^\infty$ (which is contractible) as follows. First take two points, which is $S^0$. Then glue on two paths (1-discs) connecting them, to make $S^1$. Then glue on two 2-discs to form the two hemispheres of $S^2$. And so on. None of the $S^n$’s are contractible, although $S^\infty$ is, but if we stop after gluing on one of the $k$-discs for any $k$, then we end up with $D^k$ which is contractible.

This other way to define $IsEquiv$ should be attributed to a handful of people who came up with it a year ago at an informal gathering at CMU, but I don’t know the full list of names; maybe someone else can supply it.

Next time: the univalence axiom!