(Co)limits of locally cartesian closed categories

In this preprint Isaev describes a combinatorial model category which presents the $(\infty, 1)$-category of finitely complete $(\infty, 1)$-categories. The underyling category is the category of simplicial sets equipped with collections of distinguished cones over diagrams indexed by finite simplicial sets. Fibrant-cofibrant objects are precisely quasicategories with finite limits such that the marked cones are exactly the limit cones. One can also choose the notion of a marking to include witnesses for internal hom-objects in the slices (or dependent products if you prefer). This yields a combinatorial model category whose fibrant-cofibrant objects are LCC quasicategories and thus the associated $(\infty, 1)$-category is locally presentable.

Also, note that the fortegful functor to quasicategories (I wouldn't call that an inclusion) does not preserve colimits. For example the initial LCC quasicategory has one (terminal) object one while the initial quasicategory is empty.


First, a clarification: what are the morphisms of locally cartesian closed categories meant to be?

Now, a word on the "two adjoints" thing.

For every category $C$, there is a cocartesian fibration $\mathrm{cod}: C^{\Delta[1]} \to C$ with fiber $C/c$ over $c \in C$; reindexing is given by composition. $C$ has pullbacks if and only if $\mathrm{cod}$ is simultaneously a cartesian fibration (i.e. it is a bifibration); reindexing is given by pullback.

If $C$ has pullbacks, then the cartesian fibration $\mathrm{cod}$ classifies a functor $C^\mathrm{op} \to \mathsf{Cat}$. This functor is also classified by a cocartesian fibration $\overline{\mathrm{cod}}: E \to C^\mathrm{op}$ (different from $\mathrm{cod}$). In the "total category" $E$, an object over $c \in C^\mathrm{op}$ is a map $f: d \to c$ in $C$, while a morphism from $f$ to $f'$ over $\gamma: c \leftarrow c'$ is a map $c \times_d c' \to d'$. Now $C$ is locally cartesian closed if and only if the cocartesian fibration $\overline{\mathrm{cod}}$ is simultatneously a cartesian fibration. Pavlovic calls such a functor a "trifibration"; his paper is referenced in the nlab page on bifibrations linked to above.

The process of straightening a cartesian fibration and then unstraightening it to get a cocartesian fibration may sound unwieldy in the $\infty$-categorical setting, but it has been studied by Barwick, Glasman, and Nardin, and I think they give a more direct construction.

Upshot:

This allows one to check that (small) locally cartesian closed categories form a presentable category, since they lie in a pullback diagram of accessible right adjoints between such:

$\require{AMScd} \begin{CD} Cat^{lcc} @>>> Cat^{cart} \\ @VVV @VVV\\ Cat^{pb} @>>> Cat^{\Delta[1]} \end{CD}$


I was talking about the following tentative argument. The 2-category of distributors (also called profunctors) $\mathrm{Dist}$ has (small) categories for objects. For $C,D:\mathrm{Dist}$ the 2-category of morphisms is defined as $$\mathrm{Dist}(C,D):=[D^{op} \times C; Set]$$ and denoted as $C \nrightarrow D$ (the middle line should be upright, but it's hard to latex). The order of arguments is chosen for the same variance as in the $Hom$-functor. The $Hom$-functor itself is the identity arrow $C \nrightarrow D$ The composition is given by the tensor product of bifunctors, i.e. if $F: D^{op} \times C \to Set$ and $G: E^{op} \times D \to Set$, then $$G\circ F(e, c) := \int^d G(e,d) \times F(d, c)$$ The fact that $Hom$ is identity is thus equivalent to the co-Yoneda lemma. There is an embedding $i: \mathrm{Cat} \to \mathrm{Dist}$, which is identity on objects and maps a functor $F: C \to D$ to the distributor $\hat F : C \nrightarrow D$ $$\hat F(d, c) = D(d, F c)$$ The distributors coming from the functors can be described as precisely the morphisms with a right adjoint, the right adjoint given by $\hat F^!(c, d) = D(F c, d)$. The inclusion $i: \mathrm{Cat} \to \mathrm{Dist}$ itself has a right adjoint which maps a category $C$ to the presheaf category $\hat C := [C^{op}, Set]$ and the distributors to their left Kan extension along the Yoneda embedding.

A more familiar 1-categorical construction is the allegory of correspondences $\mathrm{Corr}(S)$ in a 1-topos $S$. The only difference is that in allegories people usually say that morphisms are correspondences with a left adjoint. This is an unfortunate historical error due to the fact that correspondences are symmetric in both arguments, so the choice whether the graph of a function is a correspondence from $A$ to $B$ or vice versa is arbitrary. Since the subobjects of a set form a set, the adjunction realizes $\mathrm{Corr}(S)$ as an algebraic category over $S$. For $S=Set$ this is the statement that the sets of subsets are precisely the boolean algebras. Unfortunately $\mathrm{Dist}$ doesn't seem to be algebraic or presentable over $\mathrm{Cat}$ in a naive way, since $\mathrm{Cat}$ is the category of small categories but the right adjoint maps $\mathrm{Dist}$ to large categories of presheaves. We don't even need an adjunction: presentable categories have small hom-sets while $[D^{op} \times C, Set]$ is a large category with a large core. Maybe some different notion of presentability is required?

The cartesian product $\times$ gives a symmetric monoidal structure on $\mathrm{Dist}$ and any category is dualizable (but not fully dualizable) w.r.t. this monoidal structure, the dual is the opposite category. This allows us to talk algebraically about both covariant and contravariant functors, as well as adjunctions. First let's talk about cartesian closed categories. We can encode the cartesian product as the morphism $C \times C \nrightarrow C$ which is a functor (=has right adjoint) and which is right adjoint to the diagonal $C\to C \times C$. The diagonal is a functor which arises by unversality of cartesian product w.r.t. functors. Similarly we can define a structure of $X^{\times n}$ for any $n:\mathbb{N}$. Thus we can encode a cartesian category as a tensor functor from the category which objects are finite sets with function to $\pm 1$ (negative will be required shortly) which is a tensor closed category, tensor product given by disjoint union of sets, a dual of $(\ast, +)$ is $(\ast, -)$ and vice versa, together with extra nontrivial generating morphisms which encode the functors and adjunctions in the definition of cartesian structure above. Now, any morphism $(\ast, +) \sqcup (\ast, +) \to (\ast, +)$ equivalently gives a morphism $(\ast, +) \to (\ast, -) \sqcup (\ast, +)$. The inner hom is defined by the condition that for the functor $C \times C \xrightarrow{\times} C$ this dual morphism is itself a functor, i.e. has a right adjoint. Adding the corresponding right adjoint to the classifying tensor category, we get a theory of cartesian closed categories.

Locally cartesian closed categories are defined similarly, but we need to work with arrow categories, so our tensor categories will include not only signed sets but also arbitrary signed finite categories. In particular, for lcc structure we focus on the arrow $\bullet \to \bullet$ and demand that for a fixed endpoint the overcategory has a cartesian closed structure (this will also involve diagrams of the form $\bullet \to \bullet \leftarrow \bullet$ etc). This shows that the lcc categories are equivalent to tensor functors from a certain tensor 2-category into $\mathrm{Dist}$. This would be sufficient for presentability if $\mathrm{Dist}$ was presentable, but as noted above it isn't quite so.