The n-Category Café

To help get an idea what our options might be, let’s think about the structures we see arising in set-based mathematics. As an example, I’ll consider one familiar sort of structure: groups.

One way to describe or construct a group is what I’ll call the explicit approach: we say precisely what its elements are and what the group structure is. This might take the form of a multiplication table. But more generally, I’ll call a description “explicit” if it is as explicit as its inputs. For instance, the product of two groups $G\times H$ can be defined to have elements ordered pairs $(g,h)$ with $g\in G$ and $h\in H$, and multiplication defined by $(g,h)(g',h') = (g g', h h')$; this is fully explicit in terms of the structure of $G$ and $H$.

A characteristic of an explicit description is that the different “parts” of the structure can be defined more or less separately (subject to the rules governing the structure). For instance, if $G$ happens to act on $H$ in a specified way, then the set of ordered pairs $(g,h)$ can be given a different group structure $(g,h)(g',h') = (g g', h^{g'} h')$, yielding the semidirect product $G\ltimes H$.

A different way to describe or construct a group is with a presentation, consisting of some “generating” elements and equations. An explicit description can be converted into a presentation in a fairly trivial way, but the converse is not always true: the word problem for groups is not solvable in general. This may seem to make presentations less useful than explicit descriptions, but in fact lots of interesting and important structures are known best (or only) by presentations.

So, in building our foundational system, we might consider using either explicit descriptions or presentations as ways to construct objects. For instance, I think it’s reasonable to say that material set theories (like ZFC) mostly take the explicit approach. Material-sets are determined by their elements, and most of the axioms of material set theory tell us how to construct particular sets by specifying their elements (in terms of other sets we already have).

On the other hand, both of these approaches are very reductionist, depending on the fact that our objects (such as groups) are structured sets. Thus, neither is very promising if we’re looking for a foundational system whose basic objects are not sets. So what else might we consider?

Category theory suggests another fundamental way to describe objects: with universal properties. More precisely, we can characterize something by exhibiting it as a representing object for a functor. Since functors can be covariant or contravariant, we obtain two dual sorts of characterizations: “left” universal propreties and “right” universal properties. For instance, the cartesian product of groups $G\times H$ can be characterized as a (right) representing object for the functor $Hom(-,G)\times Hom(-,H)$, while the tensor product of abelian groups $G\otimes H$ can be characterized as a (left) representing object for the functor $Bilin(G,H; -)$.

There are close connections between (1) right universal properties and explicit descriptions, and (2) left universal properties and presentations. The latter is familiar to a category theorist: the group presented by generators $S$ and relations $R$ is the coequalizer of the pair $F R \;\rightrightarrows\; F S$, where $F$ denotes the free group functor; this is precisely a left universal property. (Note, though, that this is not to say that this universal property is the same as the intuitive meaning of a “presentation” in the sense of “all the elements are obtained by applying the operations to $S$ subject to relations $R$”.) Morever, many or most left universal properties can be expressed as presentations: for instance, this is the case for the tensor product.

On the other hand, in most “categories of structures”, we can extract an explicit description fairly easily from a right universal property—because of the presence of certain special objects with left universal properties. For instance, in the case of groups we have the free group on one generator, $\mathbb{Z}$, such that $Hom(\mathbb{Z},G)$ is the underlying set of $G$. It follows immediately that if $G\times H$ is defined using the (right) universal property of a product, then its underlying set must be the cartesian product of those of $G$ and $H$; and so on. Many explicit descriptions can be expressed as right universal properties, but sometimes this is tricky; for instance, what is the universal property of the semidirect product? (There are answers; I’m just saying they are less obvious, and in other cases they may be even harder.)

So, returning to our foundational system, we might alternatively consider expressing constructions in terms of universal properties. This is pretty clearly the choice made by structural set theories such as ETCS. In fact, the axioms of ETCS are usually expressed exactly in terms of universal properties in the category of sets.

If we’re hoping to free ourselves from sets, this approach is more promising, but it still has a drawback: universal properties are usually expressed in terms of (natural) bijections of hom-sets. ETCS deals with this by shifting the statement of universal properties into the ambient first-order logic. That is, instead of characterizing the product of sets $A\times B$ by a natural bijection $Hom(-,A\times B)\cong Hom(-,A)\times Hom(-,B)$, we have instead axioms which say that “for every $f:X\to A$ and $g:X\to B$, there exists a unique $h:X\to A\times B$ such that …”. While this does avoid circularity, it more or less forces the notions like “uniqueness” used in these universal properties to be those of the ambient first-order logic. Thus, if this logic is of the traditional sort, this means that there is still a “set-like” structure hanging around somewhere.

Fortunately, we can make one further improvement that helps resolve this problem. It’s well-known that in a closed category (perhaps monoidal, or cartesian, or whatever is appropriate), universal properties can usually be “internalized”. For instance, the exponential object $Z^Y$ in a cartesian closed category is characterized by natural isomorphisms

$$Hom(X, Z^Y) \cong Hom(X\times Y, Z)$$

but this automatically implies that we also have isomorphisms of exponential objects

$$(Z^Y)^X \cong Z^{X\times Y}.$$

This latter property seems more amenable to being expressed in a foundational system without needing any ambient set-like structure. It’s a long way from there to actually finding such a foundational system, but fortunately the work’s already been done for us. Of course, as always, I’m talking about type theory.

In type theory, the basic objects are types and their elements. Traditionally, one thinks of types as being like sets, and that’s sometimes a very helpful guide when reasoning in type theory. However, the essential point today is that types don’t have to be like sets.

In order to explain how type theory expresses definitions by universal properties “internally”, I need to say something about how it handles variables. In set-theoretic foundations, if I have a variable $x$ and an expression involving $x$, I can substitute any value for $x$ and the expression will then denote a resulting value. For instance, the expression $x^2+1$ denotes $5$ when I substitute $2$ for $x$. Thus, an expression containing a free variable $x$ implicitly describes a “function” of sorts, from input values to output values.

This is also true in type theory, but because types might be more structured than sets are, an expression containing a free variable does not merely describe a function (between sets), but a morphism (between types). One way to think of this is that the “elements” of a type act more like generalized elements in category theory. Another way to think of it is that we should be able to “substitute” for a variable not just the “values” in its domain in the naive sense (e.g. the elements of the underlying set of a group), but also whatever structure there may be relating those values, to ensure that the “morphism” defined by any expression preserves that structure.

The practical upshot of this is that we can express rules for constructing types in terms of their “elements”, and then these rules will automatically characterize those types by a full universal property with respect to all “morphisms”. For instance, one of the rules for cartesian product types says that “if we have elements $a:A$ and $b:B$, then we can form an element $(a,b):A\times B$.” Since these elements $a$ and $b$ may involve free variables, this implies automatically that any pair of morphisms into $A$ and $B$ also yield a morphism into $A\times B$.

This should be contrasted with the treatment in material set theory, where $A\times B$ is defined explicitly in terms of its elements $(a,b)$, and in order to prove its universal property in the category of sets we have to say something like “given $f:X\to A$ and $g:X\to B$, for any $x\in X$ we have elements $f(x)\in A$ and $g(x)\in B$, hence we can form the pair $(f(x),g(x))$, and we define $h:X\to A\times B$ to send $x$ to $(f(x),g(x))$.” The latter argument depends on knowing that sets “have no structure”; if we wanted to do the same thing in the category of groups, we would have to add an additional part verifying that $h$ is a group homomorphism. In type theory, all the extra structure that types might have is handled automatically by the interpretation of variables.

Nearly every rule for constructing types in type theory can be regarded as expressing a universal property. The division into “left” and “right” universal properties is referred to by type theorists as the division into “positive types” and “negative types”, and called generically “polarity”. In type-theoretic language, we say:

• A negative type is characterized by giving the basic ways to use an element of it. For instance, the ways to use an element of $A\times B$ are to extract its first or second component. The way to use an element of the function type $B^A$ is to apply it to an element of $A$ and obtain an element of $B$.

  Given these, it follows that the way to construct an element of such a type is to specify what happens when we use our putative element in all possible ways. For instance, the way to construct an element of $A\times B$ is to specify its two components. And the way to construct an element of $B^A$ is to give a way to make an element of $B$ under the assumption of an element of $A$, i.e. to give an expression of type $B$ containing a (new) free variable of type $A$.

• A positive type is characterized by giving the basic ways to construct parts of it. For instance, the ways to construct parts of the coproduct $A+B$ are to inject an element of $A$, or to inject an element of $B$. And the ways to construct a natural number are either to take $0$, or to take the successor of some other natural number (this an example of a “properly recursive” inductive type, for which some of the ways to construct new elements involve having other elements of the same type).

  Given these, it follows that the way to use an element of such a type is to specify what is to be done in all possible cases, depending on the ways that such an element might have been constructed. For instance, the way to use an element of $A+B$ is to divide into two cases, according to whether that element came from $A$ or from $B$. And the way to use a natural number is to do a proof by induction, or a definition by recursion: we divide into two cases according to whether we have $0$ or a successor, and in the latter case we can assume we’ve already dealt with the predecessor natural number.

Recalling that “elements” of a type include the information of all “generalized elements”, I think it’s not too hard to see how the rule for constructing elements of, say, $B^A$, express its universal property. Morphisms $X\to B^A$ — that is, expressions of type $B^A$ containing a variable of type $X$ — are the same as morphisms $X\times A\to B$ — that is, expressions of type $B$ containing a variable of type $A$ in addition to the variable of type $X$. (Hopefully it’s not too hard to believe that a variable of type $X\times A$ is roughly the same as a variable of type $X$ and another variable of type $A$. There’s a subtle issue here involving things called contexts, but I don’t want to get into it.) Moreover, because expressions with free variables are also how we construct elements of function types, we have immediately the internalized isomorphism $(B^A)^X \cong B^{X\times A}$. The other examples are similar.

There’s an important difference between positive and negative types, however, coming from the asymmetry that “(generalized) elements” are “maps in” rather than “maps out”. To describe a positive type, we give the basic “ways to construct elements”, but nothing requires that these be the only elements of the resulting type. For instance, if types are groups, then the coproduct type $A+B$ will be the free product of $A$ and $B$, and this contains many more elements than those coming directly from $A$ or from $B$. This is despite the fact that the coproduct type is a positive type whose “basic elements” are those coming from $A$ or from $B$, and moreover that in order to use an element of $A+B$ it suffices to deal with the two cases when it comes from $A$ and when it comes from $B$. In the types-are-groups world, there are more elements of $A+B$ than these, but because all constructions must respect group structure, anything we do with a variable of type $A+B$ is uniquely determined by what happens to the images of $A$ and $B$.

(In case you’re wondering, yes, there is a type theory whose types are groups. The category of groups is regular, which is more than sufficient for it to have an internal type theory. This type theory doesn’t have as much structure as the ones we usually use as foundations for mathematics — for instance, there are no function types, since $Grp$ is not cartesian closed — but it’s a perfectly good type theory. Even more interesting is the category of abelian groups, whose internal type theory is a form of linear logic.)

I stress this point because there seems to be a common feeling among type theorists that “there should be nothing in an inductive (positive) type except what you put into it”. Probably this belief arises from thinking of types as like sets, where there are no “operations” in sight to make new stuff out of the generating stuff that you put in. But if types aren’t like sets, then all bets are off. Indeed, the great thing about type theory, as I’ve been saying, is that it frees us to consider theories whose basic objects aren’t set-like.

Now let’s bring in the homotopy theory. Suppose that we are higher category theorists, and we’d like a “natively higher-categorical” foundation for mathematics. To keep things easy, let’s look for a foundation whose basic objects are $\infty$-groupoids — more precisely, for a type theory whose types behave like $\infty$-groupoids. Surprisingly enough, it turns out that there’s not a whole lot of work to do: up to a point, plain old ordinary type theories can easily be interpreted as being about $\infty$-groupoids rather than (say) sets.

The essential thing to note is that when we do this, the “morphisms” are automatically functors between our $\infty$-groupoids, just as in the generic case discussed above. In particular, any expression with a free variable denotes a functorial operation. This is in harmony with what we would expect from a natively category-theoretic foundation of mathematics: everything you can do or say is automatically invariant (or, more precisely, “equivariant” or “covariant”) under equivalence.

One important new thing that we can add to this homotopy type theory is a new kind of positive type. The positive types in ordinary type theory are ones that make sense in any category, and are generally inspired by the category of sets (or other set-like categories). Since sets have only elements and nothing else, to give a presentation of a set is nothing but to give some elements and some equations between them.

However, $\infty$-groupoids have all sorts of higher structure, so a “presentation” of an $\infty$-groupoid can have “generators” of arbitrary dimension: not just points, but equivalences (or paths) between them, and higher equivalences between those, and so on. Moreover, when talking about weak $\infty$-groupoids, as we generally do, we can omit the “relations” entirely, since quotienting (weakly) by a relation at level $n$ is the same as adding a generator of level $n+1$. Thus, in homotopy type theory we should have positive types that correspond to presentations of this sort.

These are called higher inductive types and I think they are the most exciting thing in the world. (-: For instance, they give us a way to import all the “spaces” considered in classical homotopy theory into homotopy type theory, incarnated as type-theoretic presentations of their fundamental $\infty$-groupoids. The higher inductive type generated by a single point and a single path from that point to itself represents (the fundamental $\infty$-groupoid of) the circle, $S^1$. We similarly have $n$-dimensional spheres, tori, manifolds, CW complexes, etc. Moreover, fundamental homotopical constructions like truncation, suspension, localization, and stabilization can all be defined as higher inductive types. So we really do have a foundational system in which the “basic objects” are $\infty$-groupoids — or homotopy types — and in which all the constructions that we want to do with them are available and characterized in a convenient way.

Let me end by introducing the famous identity type from this perspective. The classical sort of “inductive type” allows us to define not only single types, but dependent types, i.e. families of types indexed by some other type. For instance, for any type $A$, there is a family of types $Vec$ indexed by the natural numbers, such that $Vec(n)$ is the type of lists of elements of $A$ of length $n$, i.e. $Vec(n) = A\times \cdots\times A$, with $n$ factors. This family can be presented by (1) a single generator generator of $Vec(0)$, called the “empty list”, and (2) for each $a:A$ and each $l:Vec(n)$, a generator of $Vec(n+1)$, called the “cons” of $a$ and $l$. This is a perfectly good (properly recursive) presentation, a.k.a. a positive type, which makes sense whether we regard types as sets or as $\infty$-groupoids.

Identity types are another example of this sort of “inductively defined family”. Namely, given a fixed type $A$ and an element $a:A$, the identity type $Id_A(a,-)$ is a family of types indexed by $A$ itself, which is presented by a single generator of $Id_A(a,a)$, called $1_a$. Now if types are like sets, then there are never any “operations” to think about, so there is nothing in a presented type except what we put into it: thus $Id_A(a,b)$ is empty unless $a$ and $b$ are the same and otherwise it contains only $1_a$. But in other cases, of course, there is no reason to expect this to be true.

In particular, if types are $\infty$-groupoids, then a dependent type over $A$ is a functor from $A$ to the $\infty$-groupoid of $\infty$-groupoids (the universe type). This is the only thing it could possibly be; remember I said that in homotopy type theory, everything is functorial. That means that the identity type $Id_A(a,-)$ is the functor $A\to \infty Gpd$ which is freely generated by one element in $Id_A(a,a)$. What is that? By the Yoneda lemma, it’s exactly the hom-functor $Hom_A(a,-)$. In topological language, this is the space of paths in $A$ starting at $a$.

Thus, there is not really anything mysterious about of identity types, nor should it be surprising that — if we regard types as $\infty$-groupoids — there is “more in the identity type” than we put into it, any more than it should be surprising that the free product of groups contains more elements than those coming directly from the two factor groups. Of course, it’s very important in working with the formal system of homotopy type theory that we have this “internalized” way to talk about the hom-functors, and so identity types naturally play a special role. But when you come down to it, they are just another sort of inductive (positive) type: a presentation of something with a left universal property.