Chapter 9 Notes

The original definition of categories, of course, was in set-theoretic foundations, so that the collection of objects of a category formed a set (or, for large categories, a class). Over time, it became clear that all “category-theoretic” properties of objects were invariant under isomorphism, and that equality of objects in a category was not usually a very useful notion. Numerous authors [blanc:eqv-log, freyd:invar-eqv, makkai:folds, makkai:comparing] discovered that a dependently typed logic enabled formulating the definition of category without invoking any notion of equality for objects, and that the statements provable in this logic are precisely the “category-theoretic” ones that are invariant under isomorphism.

Although most of category theory appears to be invariant under isomorphism of objects and under equivalence of categories, there are some interesting exceptions, which have led to philosophical discussions about what it means to be “category-theoretic”. For instance, ct:galois was brought up by Peter May on the categories mailing list in May 2010, as a case where it matters that two categories (defined as usual in set theory) are isomorphic rather than only equivalent. The case of $†$-categories was also somewhat confounding to those advocating an isomorphism-invariant version of category theory, since the “correct” notion of sameness between objects of a $†$-category is not ordinary isomorphism but unitary isomorphism.

The fact that categories satisfying the “saturation” or “univalence” principle as in ct:category are a good notion of category in univalent foundations occurred independently to Voevodsky, Shulman, and perhaps others around the same time, and was formalized by Ahrens and Kapulkin [aks:rezk]. This framework puts all the above examples in a unified context: some precategories are categories, others are strict categories, and so on. A general theorem that “isomorphism implies equality” for a large class of algebraic structures (assuming the univalence axiom) was proven by Coquand and Danielsson; the formulation of the structure identity principle in sec:sip is due to Aczel.

Independently of philosophical considerations about category theory, Rezk [rezk01css] discovered that when defining a notion of $(\mathrm{\infty },1)$-category, it was very convenient to use not merely a set of objects with spaces of morphisms between them, but a space of objects incorporating all the equivalences and homotopies between them. This yields a very well-behaved sort of model for $(\mathrm{\infty },1)$-categories as particular simplicial spaces, which Rezk called complete Segal spaces. One especially good aspect of this model is the analogue of ct:eqv-levelwise: a map of complete Segal spaces is an equivalence just when it is a levelwise equivalence of simplicial spaces.

When interpreted in Voevodsky’s simplicial set model of univalent foundations, our precategories are similar to a truncated analogue of Rezk’s “Segal spaces”, while our categories correspond to his “complete Segal spaces”. Strict categories correspond instead to (a weakened and truncated version of) what are called “Segal categories”. It is known that Segal categories and complete Segal spaces are equivalent models for $(\mathrm{\infty },1)$-categories (see e.g. [bergner:infty-one]), so that in the simplicial set model, categories and strict categories yield “equivalent” category theories—although as we have seen, the former still have many advantages. However, in the more general categorical semantics of a higher topos, a strict category corresponds to an internal category (in the traditional sense) in the corresponding 1-topos of sheaves, while a category corresponds to a stack. The latter are generally a more appropriate sort of “category” relative to a topos.

In Rezk’s context, what we have called the “Rezk completion” corresponds to fibrant replacement in the model category for complete Segal spaces. Since this is built using a transfinite induction argument, it most closely matches our second construction as a higher inductive type. However, in higher topos models of homotopy type theory, the Rezk completion corresponds to stack completion, which can be constructed either with a transfinite induction [jt:strong-stacks] or using a Yoneda embedding [bunge:stacks-morita-internal].

Title	Chapter 9 Notes