The n-Category Café

The paper has two parts. One is written in LaTeX like a traditional math paper, using English sentences and an informal style, with “abuses of notation”, leaving trivial things to the reader, etc. However, even this part is different from most informal mathematics in that it is founded in type theory rather than (some variety of) set theory. If you’ve read this post and this post you may have some idea of what that means. Section 2 of the paper gives a very brief introduction to it, as well as to the aspects that are special to homotopy type theory (versus other kinds of type theory). We would very much appreciate feedback on readability.

The second part of the paper is a formalization in the proof assistant Coq. (This shows up as the “ancillary files” on the arXiv.) The informal and formalized parts are vaguely parallel: though they don’t match up exactly, the same main theorems occur in both. A brief discussion comparing them is in Section 9 of the informal paper. The Coq development is based on Vladimir Voevodsky’s “Foundations” library, which was the first library for doing homotopy type theory in Coq. (We’re hoping to update it later to use the new “second generation” version of the HoTT library that’s currently under development at IAS.)

Okay, enough meta, what is this paper about?

The main novelty when doing category theory in homotopy type theory is that you have more freedom in how you treat equality of objects in a category. The obvious definition of a category $A$ has a type of objects, say $A_0:Type$, and a family of types of morphisms, say $hom_A : A_0 \times A_0 \to Type$. For simplicity, we restrict ourselves to 1-categories, in which case we should require each type $hom_A(x,y)$ to be a set in the precise sense of homotopy type theory (i.e. a 0-truncated type, containing no higher homotopy). But what sort of type should $A_0$ be? The choice we make governs how equality of objects in $A$ gets treated.

If we require $A_0$ to also be a set, then we get a notion of “category” which behaves more like categories in traditional set-theoretic foundations. In such categories, we can compare objects for equality, and this “equality” behaves basically like equality always has in set theory. (In particular, two objects can be equal in only one way.) This sort of equality of objects is, in particular, stricter than isomorphism. Thus we can have objects that are unequal but isomorphic, and we can perform constructions that violate the principle of equivalence. Following Toby Bartels, we call this sort of category a strict category.

Another option, however, is to require $A_0$ to be a 1-type (that is, a 1-truncated type, behaving like a 1-groupoid) in which equality is identified with isomorphism in the category $A$. More precisely, consider the equality type $Id_{A_0}(x,y)$, which is defined for any $x,y:A_0$. Remember that in homotopy type theory, equality in general types behaves like paths in a space or equivalences in a higher groupoid, so that two points can be equal in more than one way. In this case, the equality type of $A_0$ comes with a canonical map $idtoiso: Id_{A_0}(x,y) \to iso_A(x,y)$ into the set of isomorphisms from $x$ to $y$ in the category $A$ (defined in the usual way) — we define this by “path induction”. We say that a category is saturated or univalent if this map $idtoiso$ is an equivalence, for all objects $x$ and $y$.

The name “univalent” refers to the fact that this is closely related to the univalence axiom. Specifically, the univalence axiom implies that the category of sets is saturated/univalent. Just as the univalence axiom identifies equality of types with equivalence, saturation for a category identifies equality of objects with isomorphism. One must emphasize, however, that relative to set theory, it does this by expanding the notion of “equality” to coincide with isomorphism, rather than restricting the notion of isomorphism to coincide with equality.

Saturated categories always satisfy the principle of equivalence. Any construction we can perform in type theory must respect the equality types — that’s essentially what the principle of path induction says. Thus, since in a saturated category, equality of objects is identified with isomorphism, it follows that any construction we can perform must also respect isomorphism of objects. So working with a saturated category provides an ironclad guarantee of “non-evilness”: if you can state your definition or prove your theorem for saturated categories in HoTT, then it is automatically isomorphism-invariant.

Saturated categories also satisfy their own, categorified version of univalence: if two saturated categories are equivalent (in any of the the usual senses of “equivalence of categories”), then they are equal. Thus, any construction on saturated categories must also satisfy the principle of equivalence. There is no notion of “equality” or even “isomorphism” of saturated categories that is stronger than equivalence.

Saturated categories have other good properties as well. For instance, consider the statement “every fully faithful and essentially surjective functor is an equivalence of categories”. In classical set theoretic foundations, this statement is equivalent to the axiom of choice. The same is true for strict categories in HoTT. However, for saturated categories, this statement is just true, without the need for any axiom of choice. It’s essentially a “functor comprehension principle”, or a categorical version of the “principle of unique choice”: if something is determined up to unique isomorphism, then by univalence it’s determined up to unique equality, and hence we don’t need any axiom of choice in order to choose it.

The thing which I like so much about this approach is that it allows multiple kinds of category theory to coexist. People who prefer to “speak no evil” can work with saturated categories, and almost all of classical category theory will work just as it does classically (or even better), since it is well-known to satisfy the principle of equivalence. On the other hand, the occasional naturally occurring examples of strict categories, such as Peter May’s by-now classic example, are not excluded through philosophical prejudice, but merely recognized as a different sort of category, one in which we have, and care about, a notion of equality for the objects which is stricter than isomorphism. Such categories seem to be rarer than univalent ones, but they are not nonexistent.

Strict categories and saturated categories live together in the world of “categories” that have no restriction imposed on their types of objects. We call these latter “precategories”, suggesting that they are the “raw material” from which one can obtain other notions of category (strict, saturated, …) by imposing conditions that determine the paths in the type of objects.

There are other possibilites as well, although we didn’t mention any of them in the paper. For instance, it is natural to consider $\dagger$-categories which are “$\dagger$-saturated”, meaning that the equality type between objects is identified with the type of unitary isomorphisms. Whatever sort of category we are considering generally determines the right notion of “sameness” between its objects, and we can then impose an axiom on our precategories identifying that notion of sameness with the equality type, ensuring that all constructions are invariant under the correct kind of sameness.

Sometimes, however, it may happen that a precategory arises naturally whose equality types are “wrong” for what we want them to be. For instance, there is a “homotopy precategory” of types, whose type of objects is the universe $Type$, and whose hom-sets are $hom(A,B) = \pi_0(A\to B)$, the 0-truncation (reflection into sets) of the function types. We might want to treat this category category-theoretically, but it is not saturated. For this reason we may want a “saturation” operation on precategories. This is the main theorem in the paper which has no counterpart in classical category theory.

There are (at least) two ways to construct the saturation of a precategory. The first is with a higher inductive type: we define the new type of objects $\hat{A_0}$ to be generated by the original type of objects $A_0$, together with a path for every isomorphism in the original category $A$, satisfying appropriate laws and truncation axioms, all of which can be expressed as higher path constructors. We didn’t do this in the paper, first because it’s long and tedious to do carefully, and second because Vladimir’s library isn’t designed for HITs.

The other way is with the Yoneda embedding. Since the category of sets is always saturated, it follows that so is any presheaf category. Thus, if we take the full image of any category inside its presheaf category, we obtain a “weakly equivalent” category which is saturated, and which is the saturation of the original category. This approach is easier to describe, although has the disadvantage of not preserving smallness.

In the paper, we call this saturation operation the Rezk completion, because it is essentially a truncated version of the replacement of a Segal space by a complete Segal space. Indeed, in the model of homotopy type theory in simplicial sets, we can almost identify precategories, strict categories, and saturated categories with 1-truncated versions of Segal spaces, Segal categories, and complete Segal spaces respectively. (The term “precategory” comes from this world as well — it was suggested in an nForum discussion as a name for “Segal space objects” internal to an $(\infty,1)$-category.)

On the other hand, in higher topos semantics, strict categories are basically internal categories in a 1-category of sheaves (of sets), while saturated categories are stacks, and the Rezk completion is the stack completion.

So the notion of saturated/univalent category not only unifies philosophical divides in ordinary category theory, it matches them up with appropriate definitions of higher category and higher stacks.