$\newcommand{\POWER}[1]{\mathcal{P}(#1)} \newcommand{\FS}{\rightarrow} \newcommand{\CCC}{\mathsf{C}} $Background. I'm interested in the relationship between two basic and well-known categorical constructs, the contravariant powerset functor, and cartesian closedness. Both are ubiquitous and in particular, the category of sets and functions has both. I think that the question below must have been resolved a long time ago, but I could not find anything online and in the books I consulted.
Recall that the contravariant powerset functor $\POWER{\cdot}$ maps sets to their powersets, and functions $f: A \FS B$ to $\POWER{f} : \POWER{B} \FS \POWER{A}$ to their 'inverses' like this: $S \mapsto \{a \in A\ |\ fa \in S\}$.
A category $\CCC$ is cartesian closed if any finite family of objects has a product in $\CCC$, and any two objects $A$ and $B$ from $\CCC$ have an exponential object $B^A$ in $\CCC$. In particular (and simplifying a bit), there is an natural family of evaluation morphisms $ev_{ABC}$ from $A \FS (B \FS C)$ to $(A \times B) \FS C$ that is iso.
Question. What is known about the combination of cartesian-closed structure and the contravariant powerset functor? Do they go well together with each other or not? In particular, how to $\POWER{\cdot}$ and $ev$ relate?
In $\mathbf{Set}$, we have the standard result that $\mathcal{P}X\cong\mathbf{2}^X$ where $\mathbf{2}\cong\{0,1\}$. This generalizes to any elementary topos where $\mathbf{2}$ is replaced by $\Omega$, the subobject classifier (which is $\mathbf{2}$ in $\mathbf{Set}$). An elementary topos can be defined as a finitely complete category with power objects. We can then show that $\mathcal{P}1$, the power object of the terminal object, is a subobject classifier, i.e. $\Omega$, and then we can show that $\mathcal{P}X\cong\Omega^X$ in general. We can further show that the category is cartesian closed, roughly by mimicking the set-theoretic definition of functions as graphs.
Deriving all this (and much more) from the definition of elementary topos is a very good exercise, and is covered in any introduction to topos theory.