An isomorphism of categories (This question was originally asked https://math.stackexchange.com/questions/725421/an-isomorphism-of-categories, with no affirmative answer there.)
Let $C$ be an (finite) extensive category with terminal object $1$. Let $I$ be an index category. Let $j: \mathrm{FinSet}\to C$ be the  coproduct-preserving functor induced by $*\mapsto 1$. Let $f$ be a finite sets-valued presheaf on $I$, that is a functor $I^{op}\to \mathrm{FinSet}$. Let $F$ be the associated category of elements.
There is a canonical functor $[I^{op},C]→[F^{op},C]$, induced by the projection $F\to I$. It has a left adjoint that sends the terminal object in $[F^{op},C]$ to $j(f)$. So there is a canonical functor 
$$
[F^{op}, C]\to[I^{op}, C]/j(f).
$$
My question: is this an isomorphism of categories? I have a not-so-vigorous argument why this should hold, I would also like to known if this is proven some where (at least for $C=Sets$).
 A: I think I have finally understood your question.
$\require{AMScd}
\newcommand{\mor}[3]{#1 \colon #2 \rightarrow #3}%
\newcommand{\catl}[1]{\mathbb{#1}}%
\newcommand{\catw}[1] {\mathbf{#1}}%$
Since $\catw{FinSet}$ is a free finite coproduct cocompletion of the terminal category $1$, every functor $\mor{A}{1}{\catl{C}}$ to a category $\catl{C}$ with finite coproducts, uniquely extends to a coproduct-preserving functor $\mor{(-) \otimes A}{\catw{FinSet}}{\catl{C}}$, which assigns to a finite set $X$ the tensor $X \otimes A = \coprod_X A$. In particular if $\catl{C}$ has terminal object $1$, there is a functor:
$$\mor{(-) \otimes 1}{\catw{FinSet}}{\catl{C}}$$
which was denoted by $j$ in the question.
I shall rephrase your statement in terms of copresheaves, because I think it is a more natural setting (to move back to your original question just put $\catl{J} = \catl{I}^{op}$). So, let:
$$\mor{f}{\catl{J}}{\catw{FinSet}}$$
be a copresheaf on finite sets. There is a corresponding discrete opfibration given by the (op)Grothendieck construction:
$$\mor{\pi_f}{\int f}{\catl{J}}$$
The total category $\int f$ may be expressed via the coend:
$$\int f = \int^{j\in \catl{J}} f(j) \times j/\catl{J}$$
We have to show that:
$$[\int f, \catl{C}] \approx [\catl{J}, \catl{C}]/{(-) \otimes 1}$$
By universal properties, there are isomorphisms:
$$[\int^{j\in \catl{J}} f(j) \times j/\catl{J}, \catl{C}] \approx \int_{j\in \catl{J}}[f(j) \times j/\catl{J}, \catl{C}] \approx \int_{j\in \catl{J}}[j/\catl{J}, \catl{C}^{f(j)}]$$
If we assume that $\catl{C}$ is finitely extensive, then $\catl{C}^{f(j)} \approx \catl{C}/{\coprod_{f(j)} 1} = \catl{C}/{f(j) \otimes 1}$, and so:
$$\int_{j\in \catl{J}}[j/\catl{J}, \catl{C}^{f(j)}] \approx \int_{j\in \catl{J}}[j/\catl{J}, \catl{C}/{f(j) \otimes 1}] \approx [(-)/\catl{J}, \catl{C}/{f(-) \otimes 1}]$$
There should be a high-level argument showing that:
$$[(-)/\catl{J}, \catl{C}/{f(-) \otimes 1}] \approx [\catl{J}, \catl{C}]/{f(-) \otimes 1}$$
but I am not seeing it at the moment. In fact, there is a subtle problem here --- the functor:
$$j \mapsto \catl{C}/{f(j) \otimes 1}$$
from the definition of extensivity is not the usual slice functor, which has type $\catl{J} \rightarrow \catw{Cat}$. Our functor has type $\catl{J}^{op} \rightarrow \catw{Cat}$ and is defined as a component-wise right adjoint to the usual slice functor.
Nonetheless, it is relatively easy to verify the claim.
In one direction let us assume, that we are given a functor $\mor{G}{\catl{J}}{\catl{C}}$ and a natural transformation $\mor{\alpha}{G}{f(-)\otimes 1}$. We shall define a natural family of functors $\mor{H_X}{X/\catl{J}}{\catl{C}/{f(X)\otimes 1}}$ as follows:


*

*on objects: $H_X(X \overset{h}\rightarrow A) = (\catl{C}/{f(h)\otimes 1})(\lambda_A)$

*on morphisms $A \overset{s}\rightarrow B$ such that $s \circ h = k$ under object $X$: as the unique factorisation of morphism $G(s)$ through pullback $H_X(k)$   


In the other direction, let us assume that a natural family of functors $\mor{H_X}{X/\catl{J}}{\catl{C}/{f(X)\otimes 1}}$ is given. One may construct a functor $\mor{G}{\catl{J}}{\catl{C}}$:


*

*$G(A) = \mathit{dom}(H_X(\mathit{id}_X))$

*$G(A \overset{s}\rightarrow B) = \pi_{G(B)} \circ H_A(s)$, where $\pi_{G(B)}$ is the pullback projection on $G(B)$


and a natural transformation $\mor{\alpha}{G}{f(-)\otimes 1}$ by putting $\lambda_X = H_X(\mathit{id}_X)$.
Another way to see the above equivalence, is to apply the Grothendieck construction to functor $(-)/\catl{J}$ and to functor $\catl{C}/{f(-) \otimes 1}$. The first functor yields the domain fibration $\mor{\delta_0}{\catl{J}^2}{\catl{J}}$, and the second functor yields a "subfibration" $\mor{\delta_1}{\int \catl{C}/{f(-) \otimes 1}}{\catl{J}}$ of the codomain fibration $\catl{C}^2 \rightarrow \catl{C}$. Natural transformations $[(-)/\catl{J}, \catl{C}/{f(-) \otimes 1}]$ are tantamount to fibred functors $H$:
$$\begin{CD}
\catl{J}^2 @>{H}>> \int\catl{C}/{f(-) \otimes 1}\\
@V\delta_0VV @VV\delta_1V \\
\catl{J} @= \catl{J}
\end{CD}$$
Functor $H$ maps a diagram:
$$\begin{CD}
X @>{h}>> A\\
@V{\mathit{id}_X}VV @VV{\mathit{id}_A}V \\
X @>{h}>> A
\end{CD}$$
to the diagram:
$$\begin{CD}
G(X) = H(X) @>{G(h) = H(h)}>> G(A) = H(A)\\
@V{\lambda_X = H(\mathit{id}_X)}VV @VV{\lambda_A = H(\mathit{id}_A)}V \\
f(X) \otimes 1 @>{f(h) \otimes 1}>> f(A) \otimes 1
\end{CD}$$
which induces a functor $\mor{G}{\catl{J}}{\catl{C}}$ and a natural transformation $\mor{\lambda}{G}{f(-)\otimes 1}$. 
A: In the $Set$ case the assertion says 
$$[I^{op}, Set]/f \cong [F^{op}, Set]$$
where $F$ is the category of elements of $f$ per your notation. This isomorphism is easy to see if you switch to discrete fibrations via grotherndieck construction. For, than it becomes 
$$\textbf{Dfib}(I)/(F \to I) \cong \textbf{Dfib}(F)$$
For any discrete fibration $F \to I$, this follows from properties of discrete fibrations: Given $f\circ g = k$, if $f$ and $g$ are d.f. then so is $k$, and if $f$ and $k$ are d.f. then so is $g$.
Anyway this is probably what the answer in one of your links explains.
