A step in Lurie's treatment of $L$-theory I am looking at Proposition 3 of Lecture 6 from Lurie's course Algebraic L-theory and Surgery (https://www.math.ias.edu/~lurie/287xnotes/Lecture6.pdf).  This involves a stable $\infty$-category $\mathcal{C}$, a finite set $S$, and a diagram of objects $X(T)\in\mathcal{C}$ indexed by nonempty subsets $T\subseteq S$ with restriction maps $X(T)\to X(U)$ when $\emptyset\neq U\subseteq T\subseteq S$.  (All this is to be interpreted in the usual $\infty$-categorical way.) I'll take $S=\{0,1,2\}$ and write $X_{01}$ for $X(\{0,1\})$ and so on.  I'll also define $X_\emptyset$ to be the colimit of $X(T)$ for $T\neq\emptyset$, so we have a homotopy cocartesian cubical diagram as follows.

We now define $Y(T)$ to be the colimit of $X(U)$ over nonempty subsets $U\subseteq T$, except that in the case $T=\emptyset$ we define $Y(\emptyset)=X(S)$.  This means that
\begin{align*}
 Y_\emptyset &= X_{012} \\
 Y_0 &= X_0 & Y_1 &= X_1 & Y_2 &= X_2 \\
 Y_{01} &= X_0\cup_{X_{01}}X_1 & 
 Y_{02} &= X_0\cup_{X_{02}}X_2 & 
 Y_{12} &= X_1\cup_{X_{12}}X_2 \\
 Y_{012} &= X_\emptyset
\end{align*}
One can check that these fit together into a new cubical diagram as follows.

Lurie states that this is again homotopy cocartesian (and hence also homotopy cartesian by stability, which is what he really wants).  He says that this follows ``by unwinding the definitions'', and spells out how it works in the case $|S|=2$, where it is indeed obvious.  The corresponding statement for classical colimits in the category of sets is also not very hard, but here we are essentially looking at a homotopy colimit, which is more subtle.  Consider, for example, the case where $X_{012}=A$ and $X(T)=0$ for $\emptyset\neq T\neq\{0,1,2\}$, which gives $X_\emptyset=\Sigma^2A$.  We find that $Y(T)$ is also zero for $\emptyset\neq T\neq\{0,1,2\}$ and so the claimed conclusion is true but things do not fit together in a very obvious way.
I think that I can see a proof of the claim involving a bit of a detour, but it is not consistent with the claim that we just need to unfold the definitions.  Can anyone suggest a better way to think about this?
 A: Here is a way to see it which might constitute "just unfolding the definitions" (at least if one were sitting in on the class at Harvard when it was being taught).
Set $Z(T) = Y(T^c)$, (compliment taken in $S$). Then the cube of $X$'s and the cube of $Z$'s are indexed on the same thing, making it easier to compare.
Consider the colimit of the $Z(T)$'s. We have:
$$ \varinjlim_{\substack{T \subseteq S \\ T \neq \emptyset}} Z(T) =\varinjlim_{\substack{T \subseteq S \\ T \neq \emptyset}} Y(T^c) =  \varinjlim_{\substack{T \subseteq S \\ T \neq \emptyset}}  \varinjlim_{\substack{U \subseteq S \\ U \neq \emptyset \\ \textrm{either } U \subseteq T^c \\ \textrm{ or } T=S=U  }} X(U)$$
$$  =  \varinjlim_{\substack{T, U \subseteq S \\ T, U \neq \emptyset \\ \textrm{either } T \cap U = \emptyset} \\ \textrm{ or } T=S=U } X(U)  \stackrel{\star}{=}  \varinjlim_{\substack{U \subseteq S \\ U \neq \emptyset}} X(U)  \cong X_\emptyset = Z_\emptyset$$
This is what we wanted to show.
(Quick aside, I wish I knew how to make a proper colimit operation with MathJax).
The only identification that is non-trivial is $\star$, and this uses an $\infty$-finality argument.
There is a forgetful functor from the strange category of pairs to the category of non-empty subsets of $S$ which just remembers the subset $U$. I claim that this is an $\infty$-final functor (cofinal in Lurie's HTT terminology). Then, since the functor of which we are taking the colimit on the left-hand side of the $\star$ factors through this forgetful functor, we have that $\star$ is an equivalence.
To see that the forgetful functor is $\infty$-final, we need to see that certain under categories have contractible classifying spaces (see the n-lab page on $\infty$-final functors for some details, especially thm 4.2). Specifically, we may fix $U_0$ and then consider the category of non-empty pairs $(U,T)$ such that $U \subseteq U_0$ and either $U=T =S$ or $U$ and $T$ are disjoint. The former can only happen when $U_0=S$, and in this case there is an initial object $U=T=S$ (morphisms are the reverse of inclusions). So that case has contractible classifying space, and we must show the same is true for $U_0 \neq S$.
For $U_0 \neq S$ we have a zig-zag of natural transformations between functors: (here we denote their value on a pair $(U,T)$, the first is the identity functor, the last is the constant functor):
$$ (U,T) \leftarrow (U, T \cup U_0^c) \to (U, U_0^c) \leftarrow (U_0, U^c_0) $$
This shows that the classifying space of these under categories is indeed contractible, so that the forgetful functor is $\infty$-final, as claimed.
