Remark Pseudocategories and categories of categories [efr-001O]

We will want to say that the category of pseudo double categories is the category of internal pseudocategories---modeled as Segal objects---in the bicategory of categories. There are two issues with this statement as written.

First of all, a priori, a weak Segal category is quite different from a pseudo double category. Not only is there not a canonical choice of composition given two horizontal maps f: x \nrightarrow y, g: y \nrightarrow z, we cannot even (a priori) guarantee the existence of a choice of composition gf which has the right boundaries on the nose---only up to vertical isomorphism (so we can find a composite x' \nrightarrow y' and isomorphisms x \cong x', y \cong y'). On the other hand, a weak Segal category is also stronger than a pseudo double category, in the sense that every vertical isomorphism has a companion.

We will see that the first defect can always be remedied after replacing our weak Segal category with an equivalent one. The issue of companions is a fundamental difference, but luckily all of the relevant double categories we want to consider have these companion pairs.

The second question is somewhat subtler (but also less important). The category of internal pseudocategories, computed in any higher category, has a priori the same homotopy level as the input---just as the category of monoids is a 1-category (like \mathsf {Set},) but the category of monoidal categories is a bicategory. This makes sense if we view categories as just a plain (generalized) algebraic theory, but we usually want to think of categories of categories as having some extra homotopy theory coming from the category structure---the category of categories in \mathsf {Set} is a bicategory (actually a 2-category, i.e it's strict), not a plain category. The preceding construction does not account for this---the homotopy limits implicit in the phrase "a pseudocategory in pseudo double categories" are, for us, merely homotopy limits of plain categories, not accounting for the extra categorical structure in a double category.

It is not clear what this means in general (and in any case, our output category will actually be strict in two directions,) but it is an important subtlety to remember.

(A category viewed as an object merely of the 1-category of categories is sometimes called a strict category, but obviously we can't speak about "strict pseudo double categories")