# Model independent proof of colimit formula for left Kan extensions

I am interested in finding a proof of the colimit formula for left Kan extensions $(\infty,1)$-categories which does not rely on a chosen model. (By a model inpendent proof I mean a proof which uses only categorical reasoning, which should be able to be performed in any given model + straightening/unstraightening).

Moreover, I would like to prove the reciproque: If the considered colimits exist in the target category then the left Kan extension exists and is given by the colimit formula. I've tried different approaches, namely:

1. Establishing the coend formula: However, to give a proof of this result, one needs to establish first the end formula for natural transformations, and it seems that a model independent of this fact cannot be given, since at some point one needs to do some calculations, which cannot be done in a model-free way. (For a reference of the end formula for natural transformations, using the theory of quasicategories, one has http://arxiv.org/pdf/1501.02161.pdf)

2. The colimit formula would follow from the Beck-Chevalley condition for coCartesian fibrations. However, even though that Lurie's HTT has a treatment about this, a model independent proof of this seems far from reachable.

3. To explicitly construct a functor, whose on objects would give the desired colimit formula, satisfying the universal property for LKE, using straightening/unstraightening in a clever way. But still, to prove such result, one needs to explicit do some calculations which do not seem at all feasible, even if one adopts a given model, (e.g., quasicategories).

Even if such approaches seem to be in vain, I am convinced that it should be possible to give a model independent proof of this result.

• I am not convinced a model-independent proof exists. Even for ordinary categories, a fair amount of machinery is needed, all of which ultimately boil down to calculations of ends in $\mathbf{Set}$. – Zhen Lin Nov 16 '15 at 12:44
• The twisted arrow category is model independent and the formula you're looking for is the limit over the twisted arrow category, right? – Dylan Wilson Nov 16 '15 at 19:48
• You mean the end formula for natural transformations? How do you prove this model independently? – Jorge António Nov 16 '15 at 22:30
• I think I'm confused by what "model independently" means. The twisted arrow category is model independent, colimits and such are model independent, fibrations and bifibrations are model indepedent... what is the precise thing you take issue with here? For example, in section 5 of the paper you cite, where do we use particular facts about the quasi-category model, for example? – Dylan Wilson Nov 17 '15 at 17:37

Dominic Verity and I have been working to develop model independent foundations of $(\infty,1)$-category theory. Our aim at present isn't to cover all models of $(\infty,1)$-categories but only the "best-behaved ones" (which include quasi-categories, complete Segal spaces, Segal categories, and naturally marked simplicial sets). The benefit to restricting to these models is that it allows us to work more strictly so that the development of the basic category theory is more similar to that for ordinary 1-categories, working in the strict 2-category CAT. A survey of the present state of this project can be found here:

$\infty$-category theory from scratch

Let me now sketch how our approach deals with Kan extensions. The details can be found in section 5 of our most recent paper:

Kan extensions and the calculus of modules for $\infty$-categories

For each of the well-behaved models of $(\infty,1)$-categories there is a strict 2-category whose objects are the $(\infty,1)$-categories of this variety, whose morphisms are the $(\infty,1)$-functors, and whose 2-cells I'll call natural transformations. For concision let me now call the objects and morphisms $\infty$-categories and $\infty$-functors. We call this the homotopy 2-category because it can be thought of as a categorification of the usual homotopy category associated to a model category. The homotopy 2-categories defined for each of the four models mentioned above are connected by 2-functors that are biequivalences. Each homotopy 2-category has certain additional structures that are derived from a common axiomatization which we use to develop the theory of $\infty$-categories: namely each of the well-behaved models defines what we call an $\infty$-cosmos. Everything is proven relative to the $\infty$-cosmos axiomatization, which is why this approach is "model agnostic."

Some pleasant features of the homotopy 2-category is that the equivalences and adjunctions in there are exactly the correct notions, meaning they recover the model-theoretic notions of weak equivalence between $\infty$-categories and also Lurie's notion of adjunctions in the case of quasi-categories (though this isn't obvious). Inside the homotopy 2-category you can also define (co)cartesian fibrations (which again specialize to the Lurie ones in the case of quasi-categories) and also define limits and colimits of diagrams valued in an $\infty$-category indexed by either a simplicial set or by another small $\infty$-category (because the models just mentioned happen to all be cartesian closed).

Now Kan extensions of one $\infty$-functor along another can also be defined in any 2-category but some care is needed here. The universal property of being a mere Kan extension in the homotopy 2-category is not strong enough: instead the correct notion is of a pointwise Kan extension. We give two equivalent definitions of this notion but the simplest for the present purpose is that a Kan extension of an $\infty$-functor $f \colon A \to C$ along an $\infty$-functor $k \colon A \to B$ is pointwise if when you paste an exact square whose bottom edge is $k$ on top, the result is still a Kan extension. Exact squares are squares with a natural transformation in them that are characterized by a property that makes use of the modules of the title.

Examples of exact squares include pullback squares one of whose edges is (co)cartesian; perhaps this is the Beck-Chevalley result you were referring to? Another example of an exact square is a comma square. This proves the easy half of the colimit formula for left Kan extensions that you were referring to: the value of the pointwise left Kan extension of $f$ along $k$ at some $b : 1 \to B$ is given by the limit of the restriction of $f$ along the projection $k \downarrow b \to A$.

The converse direction is more subtle because we need to assemble these colimit values, one for each "object" $b$ in $B$, into an $\infty$-functor $lan_k f : B \to C$. What's needed to do this is something like the principle that "universal properties for $\infty$-categories are determined objectwise." For quasi-categories, we prove a precise theorem expressing this idea. The proof involves some horn-filling inductive argument over simplices, so it's very particular to the quasi-categorical model. In the very last part of our paper, we use this to sketch a proof that any cocomplete quasi-category has all Kan extensions of small functors given by the colimit formula (full details will appear in our forthcoming sixth paper, which specializes to the quasi-categorical case).

Because our argument uses the quasi-categorical model there is some model independence lost at this step, but happily it's only lost in the proof, not in the conclusion. The reason for this is a model independence theorem (which is sketched in the "scratch" lecture notes and will be presented in more detail in our forthcoming seventh paper, on model independence). Not only are the homotopy 2-categories for the models mentioned above biequivalent, but there is a more sophisticated categorical structure called a virtual equipment that we construct for each model, and these virtual equipments are also biequivalent. The virtual equipment encodes the "calculus of modules" for $\infty$-categories; in particular, this captures the universal properties of cartesian fibrations and Kan extensions and the like. So the "universal properties for $\infty$-categories are determined objectwise" result also holds for the other models and the rest of our argument (which takes place in the virtual equipment) now applies.

Sorry for the length of this post!