I'm trying to fill in the details of the proof and need the following result: $Set^{C^{op}}/P\simeq Set^{D^{op}}$, where $D$ is the category of elements of $P$. The objects are pairs $(x,C)$ with $C ∈ C $and we may take (by Yoneda) $x ∈PC$ to be $x : yC → P$ and then the arrows are just morphisms $\vartheta :x\rightarrow x'$ in the slice category $yC/P$. ($C$ ranges over $C$).
We need functors $F$ and $G$ s.t $GF\cong 1_{Set^{C^{op}}/P}$ and $FG\cong 1_{Set^{D^{op}}}$ One way is fairly obvious:
$F: Set^{C^{op}}/P \rightarrow Set^{D^{op}}$ defined by $F(q)(C, x) = Hom_{Set^{C^{op}}/P}(x, q)$
But what should the functor $G:Set^{D^{op}}\rightarrow Set^{C^{op}}/P$ be?
edit: I remembered a similar construction when proving that $Set^{I}\simeq Set/I$ so I'm just mimicking it:
I let $G$ be defined as follows: if $h∈Set^{D^{op}}$, then take $r∈ Set^{C^{op}}$ to be $r(C)=\coprod _{x\in PC}h(C,x)$, where we identify $x ∈PC$ with $x : yC → P$. We then just project this to $PC$ and so get an object in $Set^{C^{op}}/P$, namely $\pi :r\rightarrow p$.
But now I have a question. In the proof I was following, the category of elements of $P$ was taken to be as described above. But wouldn't it be easier to just use the normal definition? Because then, if $q:Y\rightarrow P$, you can just take $F: Set^{C^{op}}/P \rightarrow Set^{D^{op}}$ to be $F(q)(C, x)=q_{c}^{-1}(x))$ This seems easier to understand.
Is this correct?