For a quasicategory $C$, why is $\mathrm{Fun}(\Lambda^2_0,C) \to \mathrm{Fun}(\Delta^{\{2\}},C) \cong C$ a cocartesian fibration?

Question

More generally, I expect that the following is true:

Let $D$ be a diagram quasicategory, let $d \in D$ be a vertex, and use this to define $D' = D \amalg_{\Delta^{\{0\}}} \Delta^1$. Then $\mathrm{Fun}(D',C) \to \mathrm{Fun}(\Delta^{\{1\}},C) \cong C$ is a cocartesian fibration.

(This follows from Corollary 2.4.7.12 of Higher Topos Theory when $D$ is a point.)

Note that $D'$ will not generally be a quasicategory, but it will generate a quasicategory $\tilde{D'}$ (i.e. $D' \stackrel{\approx}{\rightarrowtail} \tilde{D'}$ in the Joyal model structure) such that the restriction map $\mathrm{Fun}(\tilde{D'},C) \to \mathrm{Fun}(D',C)$ is a categorical equivalence (probably even a categorical fibration). Either of these computes the Joyal-homotopy pushout of $D \xleftarrow{d} \Delta^{\{0\}} \to \Delta^1$, which should be thought of as "freely adding a morphism to $D$ with source $d$".

This fact is sufficiently obvious in 1-categories that people generally assert it without proof, but the intuition is the same: given a map $x \xrightarrow{f} y$ in $C$ and a functor $F : D' \to C$ restricting to some map $\Delta^1 \to C$ selecting an edge $a \xrightarrow{g} x$, a cocartesian lift should be given by the functor $f_*F$ which agrees with $F$ on $D$, takes $\Delta^{\{1\}}$ to $y$, and takes the edge $\Delta^1$ to a composite $a \xrightarrow{fg} y$.

---

I have an incomplete attempt at a proof of the statement in this form. Really I would prefer an "invariant" argument, i.e. one that runs in the quasicategory of quasicategories, but of course anything would be better than nothing.

The key observation is that this is true in case that $D$ is a point, i.e. it's true of the cocartesian fibration $\mathrm{Fun}(\Delta^1,C) \to \mathrm{Fun}(\Delta^{\{1\}},C) \cong C$: more precisely, given an edge $x \xrightarrow{f} y$ of $C$ and a point $a \xrightarrow{g} x$ of the fiber over $x$, there is a cocartesian edge $\Delta^1 \to \mathrm{Fun}(\Delta^1,C)$ described by a commutative square

$$\require{AMScd} \begin{CD} a @= a \\ @VV{g}V @VV{f g}V \\ x @>>{f}> y \end{CD}$$

(where the un-drawn lower-left $\Delta^2$ is a composition and the un-drawn upper-right $\Delta^2$ is degenerate, and the outer and inner copies of $\Delta^1$ correspond to the horizontal and vertical directions, resp.). Let me write $\tilde{f}$ for this edge of $\mathrm{Fun}(\Delta^1,C)$. Now, note that $$ \mathrm{Fun}(D',C) \cong \mathrm{Fun}(D \amalg_{\Delta^0} \Delta^1,C) \cong \mathrm{Fun}(D,C) \times_C \mathrm{Fun}(\Delta^1,C). $$ The edge $id_{F|D}$ of the left factor agrees in $C$ with the edge $\tilde{f}$ of the right factor (both restrict to the edge $id_a$), so they define an edge of the fiber product, which I'll call $\tilde{F}$. The claim is that this edge is a cocartesian edge over $f$ with source $F$. By definition, this is the assertion that the map $$ \mathrm{Fun}(D',C)_{\tilde{F}/} \longrightarrow \mathrm{Fun}(D',C)_{F/} \times_{C_{x/}} C_{f/}$$ is a trivial Kan fibration. Unwinding the definitions, the source is $$ \mathrm{Fun}(D',C)_{\tilde{F}/} \cong \mathrm{Fun}(D \amalg_{\Delta^0} \Delta^1 , C)_{\tilde{F}/} \cong \mathrm{Fun}(D,C)_{id_{F|D}/} \times_{C_{id_a/}} \mathrm{Fun}(\Delta^1,C)_{\tilde{f}/} , $$ while the target is $$ \mathrm{Fun}(D',C)_{F/} \times_{C_{x/}} C_{f/} \cong \left( \mathrm{Fun}(D \amalg_{\Delta^0} \Delta^1 , C)_{F/} \right) \times_{C_{x/}} C_{f/}$$ $$ \cong \left( \mathrm{Fun}(D,C)_{(F|D)/} \times_{C_{a/}} \mathrm{Fun}(\Delta^1,C)_{g/} \right) \times_{C_{x/}} C_{f/} $$ $$ \cong \mathrm{Fun}(D,C)_{(F|D)/} \times_{C_{a/}} \left( \mathrm{Fun}(\Delta^1,C)_{g/} \times_{C_{x/}} C_{f/} \right) $$ (where this last reassociation comes from the fact that on both lines, the map from the inner fiber product to the base of the outer fiber product factors through the projection to the middle term $\mathrm{Fun}(\Delta^1,C)_{g/}$). Under these decompositions, the map which must be shown to be a trivial Kan fibration is given by the induced map from the pullback of the top row to the pullback of the bottom row in the diagram

$$\begin{CD} \mathrm{Fun}(D, C)_{id_{F|D} /} @>>> C_{id_{a} /} @<<< \mathrm{Fun}(\Delta^1, C)_{\tilde{f} /} \\ @VVV @VVV @VVV \\ \mathrm{Fun}(D, C)_{(F|D) /} @>>> C_{a /} @<<< \mathrm{Fun}(\Delta^1, C) \times_{C_{x /}} C_{f /} \end{CD}$$

(If we consider these as fitting into a cube where the left square here gives the front square of the cube and the right square here gives the right square of the cube, then I'm interested in showing that if we take the pullbacks of the cospans in the top and bottom faces, then the induced back-left vertical arrow is a trivial Kan fibration.)

Now, by definition of $\tilde{f}$ being cocartesian, the right vertical arrow is a trivial Kan fibration. On the other hand, I'm pretty sure the left and middle vertical arrows are trivial categorical fibrations, and that both left-hand horizontal arrows are categorical fibrations. But I don't quite see how to leverage this all into a proof of the statement I'm after. It would follow from pullback-pasting if the front square were a pullback, but I don't think that's quite true.

Answer 1

This follows from (the coCartesian version of) HTT Corollary 2.4.7.12, applied to the "evaluation at $d$" functor $\mathrm{Fun}(\mathcal{D}, \mathcal{C}) \rightarrow \mathcal{C}$, since we can identify $\mathrm{Fun}(\mathcal{D}', \mathcal{C})$ with $\mathrm{Fun}(\mathcal{D}, \mathcal{C}) \times_{\mathcal{C}} \mathrm{Fun}(\Delta^1, \mathcal{C})$, where the fibre product is via the evaluation at $0$, and the projection to $\mathcal{C}$ is via evaluation at $1$. (In fact, this is the free coCartesian fibration on the evaluation at $d$ functor.)

Answer 2

In fact, it can be shown by (a whole lot of) brute force that the morphism of cospans towards the bottom of the question is actually a Reedy acyclic fibration -- at least with respect to the Reedy structure on $\Lambda^2_2$ described by $$ (\deg = 2) \rightarrow (\deg = 1) \leftarrow (\deg = 0) . $$ Since this induces a Reedy model structure on $\mathrm{Fun}(\Lambda^2_2,\mathrm{sSet})$ for which the pullback functor $$ \lim : \mathrm{Fun}(\Lambda^2_2,\mathrm{sSet}) \rightarrow \mathrm{sSet} $$ is a right Quillen functor, this proves the necessary claim.

The full details will eventually appear in a forthcoming paper. In the meantime, I still would very much welcome an "invariant" proof of this seemingly simple fact!