How can I prove $\mathbf{1}_{Pa}=P\{\cdot\}_a\circ\{\cdot\}_{Pa}$ We have an elementary topos $\mathbf{C}$ with subobject classifier $\Omega$ and powerset functor $P:\mathbf{C}^{op}\to\mathbf{C}$, i.e, for all $\mathbf{C}$-objects $x,y$ we have
$$\mathbf{C}(x\times y,\Omega)\cong\mathbf{C}(y,Px)$$
and the bijection is natural in both variables. There are "canonical" morphisms
$$\{\cdot\}_a:a\longrightarrow Pa$$
for every object $a$. In $\mathbf{Set}$, given a set $X$, the map $\{\cdot\}_X$ maps the element $x\in X$ to the subset $\{x\}\subseteq X$ i.e the element $\{x\}\in PX$.
Every map $f:x\to x'$ transforms to a map $Pf:Px'\to Px$ by contravariance, so we have
$$a\xrightarrow{\quad\{\cdot\}_a\quad}Pa\xrightarrow{\quad\{\cdot\}_{Pa}\quad}PPa$$
$$Pa\xleftarrow{\quad P\{\cdot\}_a\quad}PPa$$
and this begs the question: is $P\{\cdot\}_a\circ\{\cdot\}_{Pa}$ the identity on $Pa$? And is $\{\cdot\}_{Pa}\circ P\{\cdot\}_a$ the identity on $PPa$?
I would like an "elementary" proof (that doesn't use adjoints or dinatural transformations or weird existence theorems). I've tried almost everything that comes to mind (writing down the diagrams takes too much time). If a dinatural transformation is unavoidable, then I don't mind it, but not adjoints by any means.
The ultimate goal of this is to prove that
$$\in_a(f\times \mathbf{1}_{Pa})=\in_{x}(\mathbf{1}_x\times Pf)$$
for any objects $a,x$ and map $f:x\to a$. The arow $\in_x:x\times Px\to\Omega$ is given by the ismorphism above. All of this is outlined in Sheaves in Geometry and Logic: A First Introduction to Topos Theory by Mac Lane and Moerdijk.
Thanks!
 A: No, even in $\mathbf{Set}$, neither composition is the identity in general.  First, if $a$ is a set, then for $S \in Pa$, $\{\cdot\}_{Pa}$ would send $S \mapsto \{ S \}$.  Then,
$$P\{\cdot\}_a ( \{ S \} ) = \{ b \in a \mid \{ b \} \in \{ S \} \} = \{ b \in a \mid \{ b \} = S \}.$$
Therefore, if $S$ has two or more elements, then $P\{\cdot\}_a \circ \{\cdot\}_{Pa}$ sends $S \mapsto \emptyset$.  Thus $P\{\cdot\}_a \circ \{\cdot\}_{Pa} \ne \mathbf{1}_{Pa}$.
(I think in fact, it should be possible to prove in a general topos that $P\{\cdot\}_a \circ \{\cdot\}_{Pa} = \mathbf{1}_{Pa}$ if and only if $a$ is a subobject of 1, i.e. if and only if the unique morphism $a \to 1$ is a monomorphism.  Any proof I can think of, however, would probably not qualify as being "elementary".  For a nontrivial example where this condition can be satisfied: in the category of sheaves on a topological space $X$, the subobjects of 1 are exactly $h_U$ for open $U \subseteq X$ -- where by definition $h_U(V) = \begin{cases}1, & V \subseteq U; \\ 0, & V \not\subseteq U.\end{cases}$  Or, if you don't believe that the base universe satisfies excluded middle, then in general $h_U(V) = (\mathcal{T}_X)(V, U) = \{ x \in 1 \mid V \subseteq U \}$ where in the middle term we're using the partial order category on the collection of open subsets of $X$.)
As for the other composition, $\{\cdot\}_{Pa}$ is certainly never surjective (for instance $\emptyset$ is never in the image), so it is impossible to have $\{\cdot\}_{Pa} \circ P\{\cdot\}_a = \mathbf{1}_{PPa}$.

As for the ultimate question of how to show
$${\in}_a(f \times \mathbf{1}_{Pa}) = {\in}_x(\mathbf{1}_x \times Pf)$$
for $f \in \mathbf{C}(x, a)$: as much as you don't want to use bifunctors, I don't see any way around using the naturality of the isomorphism of bifunctors $\mathbf{C}(x \times y, \Omega) \simeq \mathbf{C}(y, Px)$.  If we let $\Phi$ be this isomorphism, then expanding the definitions, this naturality says exactly that for $f \in \mathbf{C}(x, x')$ and $g \in \mathbf{C}(y, y')$, and $h \in \mathbf{C}(x' \times y', \Omega)$, we have:
$$\Phi_{x,y}(h \circ (f \times g)) = Pf \circ \Phi_{x',y'}(h) \circ g.$$
Now, by definition of ${\in}_a$, we have that $\Phi_{a,Pa}({\in}_a) = \mathbf{1}_{Pa}$ and similarly for ${\in}_x$.  Therefore,
$$\Phi({\in}_a \circ (f \times \mathbf{1}_{Pa})) = Pf \circ \mathbf{1}_{Pa} \circ \mathbf{1}_{Pa} = Pf.$$
Similarly,
$$\Phi({\in}_x \circ (\mathbf{1}_x \times Pf)) = P\mathbf{1}_x \circ \mathbf{1}_{Px} \circ Pf = Pf.$$
Since $\Phi$ is an isomorphism, and $\Phi$ of both sides of the desired identity evaluates to the same thing, we conclude that the desired identity is true.
