Local finality condition (for re-indexing parameterized colimits) I'm in need of a condition that is analogous to the "finality" condition in the following lemma:
Lemma: A functor $F\colon A\to B$ is final if and only if for any functor $x\colon B\to Set$, the natural map $colim (xF)\to colim(x)$ is an isomorphism.
This lemma could be taken instead as a definition of final functor, but finality is more easily recognized by whether all slice categories of a certain kind are non-empty and connected. I want a recognition principle for a more general kind of finality, which I'm calling local finality.
The more general context requires a bit of notation. If $A$ is a category, write $A-Set$ for the category of functors $A\to Set$. If $F\colon A\to B$ is a functor, write $\Delta_F\colon B-Set\to A-Set$ for the ``composition with $F$" functor, and write $\Sigma_F$ for its left adjoint and $\Pi_F$ for its right adjoint (these three are also sometimes denoted by $F^*, F_!$, and $F_*$ respectively).
The following lemma (obviously) holds for some appropriate definition of locally final. 
Lemma: Suppose that we have a commutative diagram $A\xrightarrow{F}B\xrightarrow{x}C$ and let $G:=xF$. Then $F$ is locally final if and only if the natural map $\Sigma_G\Delta_F\to\Sigma_x$ is an isomorphism.
Is there a nice recognition principle for this kind of ``local finality"? I have a big messy condition obtained by following my nose, but it's of no use. Any help would be greatly appreciated.
Thanks!
 A: Since nobody has said so, I will mention that the notion you describe is a particular case of the known --- but perhaps obscure --- concept of Guitart exact square. One can read about it in the nlab page and in an article by Maltsiniotis. Even though the latter article aims to generalize exact squares to a homotopical context, it still gives a good, if somewhat skewed, overview of the concept.
To justify the relative usefulness of exact squares, let me state that instances of that notion characterize: fully faithful functors, (co)final functors, initial functors, absolute Kan extensions, among other concepts (including my personal favourite, absolutely dense functors).
For completeness, I will summarize some characterizations of the notion of exact square. A square of small categories, functors, and natural transformations:
$$ \begin{matrix} 
A & \overset{U}{\longrightarrow} & B \\
\llap{\scriptstyle L}\Big\downarrow  & \big\Downarrow\rlap{\scriptstyle\alpha} & \Big\downarrow\rlap{\scriptstyle R} \\
A' & \underset{D}{\longrightarrow} & B'
\end{matrix} $$
(i.e. a natural transformation $\alpha:R\circ U\to D\circ L$) is called exact if any of the following equivalent conditions hold:


*


*The natural 2-cell induced by $\alpha$ in
$$ \begin{matrix} 
\textrm{Set}^A & \overset{\Delta_U}{\longleftarrow} & \textrm{Set}^B \\
\llap{\scriptstyle \Sigma_L}\Big\downarrow  & \big\Downarrow & \Big\downarrow\rlap{\scriptstyle \Sigma_R} \\
\textrm{Set}^{\smash{A'}} & \underset{\Delta_D}{\longleftarrow} & \textrm{Set}^{\smash{B'}}
\end{matrix} $$
is an isomorphism. That is, the induced natural transformation $\Sigma_L\circ\Delta_U \to \Delta_D\circ\Sigma_R$ is an isomorphism.


*For every $x\in A'$, the naturally induced functor on over-categories
$$ A/x=L/x \longrightarrow R/(D(x))=B/(D(x)) $$
is (co)final.


*For every $x\in B$, the naturally induced functor on under-categories
$$ x/A=x/U \longrightarrow (R(x))/D=(R(x))/A' $$
is initial.


*For each object $x\in B$ and $y\in A'$, and each arrow $f:R(x) \to D(y)$ in $B'$, the category of factorizations $C_{x,y,f}$ is connected (which I, Karol, and a surprisingly large/vocal set of mathematicians take to mean non-empty). Here, the category $C_{x,y,f}$ is defined by:

*

*the objects of $C_{x,y,f}$ are triples $(z,g,h)$ where $z$ is an object of $A$, $g:x\to U(z)$ is a morphism in $B$, and $h:L(z)\to y$ is a morphism of $A'$, such that $D(h)\circ\alpha_z \circ R(g)=f$;

*a morphism $(z,g,h)\to (z',g',h')$ in $C_{x,y,f}$ is an arrow $k:z\to z'$ such that $g'= U(k)\circ g$ and $h=h'\circ L(k)$.




*For all objects $x\in B$ and $y\in A'$, the natural map from the coend
$$ \int^{a\in A} B(x,U(a))\times A'(L(a),y) \longrightarrow B'(R(x),D(y)) $$
is an isomorphism of sets.



Before proceeding, observe that condition 4 is simply a restatement of conditions 2 and 3. In fact, the categories of factorizations $C_{x,y,f}$ defined in 4 are exactly the categories whose connectedness must be checked to ensure that the functor in condition 2 is cofinal (respectively, that the functor in condition 3 is initial). More precisely, the categories $C_{x,y,f}$ are the under-categories $a/F$ of the functor $F$ in condition 2 (respectively, the over-categories of the functor in condition 3) for objects $a$ in the codomain of $F$. I feel this both motivates and gives a nice way to remember the definition of $C_{x,y,f}$.
Then $A\overset{F}{\rightarrow}B\overset{x}{\rightarrow}C$ is locally final (in the sense David Spivak states) if and only if the the square
$$ \begin{matrix} 
A & \overset{F}{\longrightarrow} & B \\
\llap{\scriptstyle G}\Big\downarrow  & \big\Downarrow\rlap{\scriptstyle\textrm{id}_G}\ & \Big\downarrow\rlap{\scriptstyle x} \\
C & \underset{\textrm{id}_C}{\longrightarrow} & C
\end{matrix} $$
(filled by the the identity 2-cell on $G=x\circ F$) is exact. Under this interpretation, condition 4 above is exactly the condition given in Karol Szumiło's answer.
Addendum: To finish off, here are a few further equivalent characterizations of the exactness of the original square ($\alpha:R\circ U\to D\circ L$) drawn at the top of this answer:


*

*For any cocomplete category X, the natural 2-cell induced by $\alpha$ in
$$ \begin{matrix} 
X^A & \overset{\Delta_U}{\longleftarrow} & X^B \\
\llap{\scriptstyle \Sigma_L}\Big\downarrow  & \big\Downarrow & \Big\downarrow\rlap{\scriptstyle \Sigma_R} \\
X^{\smash{A'}} & \underset{\Delta_D}{\longleftarrow} & X^{\smash{B'}}
\end{matrix} $$
is an isomorphism. Note that for $X=\textrm{Set}$, we recover condition 1 above.

*The natural 2-cell induced by $\alpha$ in
$$ \begin{matrix} 
\textrm{Set}^A & \overset{\Pi_U}{\longrightarrow} & \textrm{Set}^B \\
\llap{\scriptstyle \Delta_L}\Big\uparrow  & \big\Uparrow & \Big\uparrow\rlap{\scriptstyle \Delta_R} \\
\textrm{Set}^{\smash{A'}} & \underset{\Pi_D}{\longrightarrow} & \textrm{Set}^{\smash{B'}}
\end{matrix} $$
is an isomorphism.

*For any complete category X, the natural 2-cell induced by $\alpha$ in
$$ \begin{matrix} 
X^A & \overset{\Pi_U}{\longrightarrow} & X^B \\
\llap{\scriptstyle \Delta_L}\Big\uparrow  & \big\Uparrow & \Big\uparrow\rlap{\scriptstyle \Delta_R} \\
X^{\smash{A'}} & \underset{\Pi_D}{\longrightarrow} & X^{\smash{B'}}
\end{matrix} $$
is an isomorphism. Note that for $X=\textrm{Set}$, we recover the preceding condition.

*The opposite square
$$ \begin{matrix} 
A^{\textrm{op}} & \overset{L^{\textrm{op}}}{\longrightarrow} & {A'}^{\textrm{op}} \\
\llap{\scriptstyle U^{\textrm{op}}}\Big\downarrow  & \big\Downarrow\rlap{\scriptstyle\alpha^{\textrm{op}}} & \Big\downarrow\rlap{\scriptstyle D^{\textrm{op}}} \\
B^{\smash{\textrm{op}}} & \underset{R^{\textrm{op}}}{\longrightarrow} & {B'}^{\smash{\textrm{op}}}
\end{matrix} $$
is exact. Note that the preceding 3 conditions and condition 1 applied to this opposite square give diagrams with categories of presheaves (contravariant functors) on $A$, $B$, $A'$, and $B'$, instead of categories of covariant functors on those categories. In fact, a common (equivalent) definition of exactness is the analog of condition 1 for presheaves: the 2-cell in the square
$$ \begin{matrix} 
\widehat{A} & \overset{\Sigma_{U^{\textrm{op}}}}{\longrightarrow} & \widehat{B} \\
\llap{\scriptstyle \Delta_{L^{\textrm{op}}}}\Big\uparrow  & \big\Downarrow\rlap{\scriptstyle} & \Big\uparrow\rlap{\scriptstyle \Delta_{R^{\textrm{op}}}} \\
\widehat{A'} & \underset{\Sigma_{D^{\textrm{op}}}}{\longrightarrow} & \widehat{B'}
\end{matrix} $$
is an isomorphism.
A: I assume you meant $\Sigma_G \Delta_F \to \Sigma_x$, otherwise this doesn't parse.
Here's my condition. It's not completely straightforward, but it is a generalization of the classical one you mentioned. I guess it's a matter of taste whether it's messy.
Consider a triple $(b, f, c)$ where $b$ is an object of $B$, $c$ is an object of $C$ and $f : x b \to c$ is a morphism in $C$. To each such triple one can associate a kind of "double slice", namely the "category of factorizations of $f$ through objects of the form $F a$". Its objects are triples $(g, a, h)$ where $a$ is an object of $A$, $g : b \to F a$ and $h : x F a \to c$ such that $h (x g) = f$. The morphisms are morphisms of $A$ making two evident triangles commute. My claim is that $\Sigma_G \Delta_F \to \Sigma_x$ is a natural isomorphism precisely when all such "categories of factorizations" are connected (which I take to include non-empty).
The argument is as follows. For any functor $W : A^\mathrm{op} \to \mathrm{Set}$ there is a $W$-weighted colimit functor $\mathrm{colim}^W : \mathrm{Set}^A \to \mathrm{Set}$ given by the coend formula $\mathrm{colim}^W Y = \int^{a \in A} Y_a \times W_a$ for $Y \in \mathrm{Set}^A$. A transformation $\phi : V \to W$ induces a transformation $\phi_* : \mathrm{colim}^V \to \mathrm{colim}^W$. It is easy to see that $\phi_*$ is an isomorphism if and only if $\phi$ is since we can recover $\phi$ form $\phi_*$ by evaluating it on representable functors.
We have formulas for Kan extensions via coends which say that $(\Sigma_x Y) c = \mathrm{colim}^{C(x -, c)} Y$ and similarly $(\Sigma_G \Delta_F Y)_c = \mathrm{colim}^{\int^a B(-, F a) \times C(x F a, c)} Y$ and the natural transformation in question is induced by the transformation $\int^a B(-, F a) \times C(x F a, c) \to C(x -, c)$ which takes a pair of morphisms $g : b \to F a$ and $h : x F a \to c$ and sends it to the composite $h (x g)$. We need to check that it is an isomorphism i.e. that the fiber over every point $f : x b \to c$ is a singleton. There is an explicit description of this coend as the quotient set of an equivalence relation and it yields a description of the fiber over $f$ as the quotient of the set of objects of the above "category of factorizations of $f$" by the relation which turns out to be the relation of being in the same component of this category.
