(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](http://ncatlab.org/nlab/show/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](http://ncatlab.org/nlab/show/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$).



An isomorphism of categories
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}$. 


