%
\label{thm:cartesian-closed}
The earned topos
$\mathcal{E}_\tau = \mathrm{PSh}(\mathrm{Cat}_\tau)$
(Definition~\ref{def:earned-topos}, I.D59)
is a \textbf{cartesian closed category}.
That is, for all presheaves $A$, $P$, $Q$
in $\mathcal{E}_\tau$:
\begin{enumerate}
    \item The internal hom $Q^P$
          (Definition~\ref{def:internal-hom}, I.D64)
          is an object of $\mathcal{E}_\tau$.
    \item The exponential adjunction holds naturally:
          \[
              \boxed{%
              \Hom_{\mathcal{E}_\tau}(A \times P,\; Q)
              \;\cong\;
              \Hom_{\mathcal{E}_\tau}(A,\; Q^P).}
          \]
    \item The evaluation morphism
          $\mathrm{ev} : Q^P \times P \to Q$
          is universal:
          every $\varphi : A \times P \to Q$
          factors uniquely as
          $\varphi = \mathrm{ev} \circ (\tilde{\varphi} \times \id_P)$
          for a unique $\tilde{\varphi} : A \to Q^P$.
\end{enumerate}

\textbf{Step 1: $Q^P$ is a presheaf.}
Definition~\ref{def:internal-hom} assigns to each $X$
the set $(Q^P)(X) = \mathrm{Nat}(y(X) \times P, Q)$.
The restriction maps are defined by precomposition,
and functoriality follows from
$y(g \circ f) = y(g) \circ y(f)$.
Thus $Q^P : \mathrm{Cat}_\tau^{\mathrm{op}} \to \mathrm{Set}$
is a well-defined presheaf.

\textbf{Step 2: The currying bijection.}
Given a natural transformation
$\varphi : A \times P \Rightarrow Q$,
define for each $X$ the map
$\tilde{\varphi}_X : A(X) \to (Q^P)(X)$
as follows.
For $a \in A(X)$,
consider the element $a$ as inducing
a morphism $y(X) \to A$
via Yoneda
(Theorem~\ref{thm:yoneda-lemma}, I.T23).
Then $\tilde{\varphi}_X(a)$ is the composite:
\[
    y(X) \times P
    \xrightarrow{\;a \times \id_P\;}
    A \times P
    \xrightarrow{\;\varphi\;}
    Q.
\]
This defines a natural transformation
$\tilde{\varphi} : A \Rightarrow Q^P$.
Conversely, given $\psi : A \Rightarrow Q^P$,
set $\varphi := \mathrm{ev} \circ (\psi \times \id_P)$.
These two maps are mutually inverse.

In the thin setting,
the bijection simplifies further.
Both sides are subterminal:
$\Hom(A \times P, Q) \in \{\varnothing, \{*\}\}$
and $\Hom(A, Q^P) \in \{\varnothing, \{*\}\}$.
The condition $A \times P \leq Q$
(i.e., $\mathrm{supp}(A) \cap \mathrm{supp}(P) \subseteq \mathrm{supp}(Q)$)
is equivalent to
$\mathrm{supp}(A) \subseteq \mathrm{supp}(Q^P)$,
which holds by the support formula
(Remark~\ref{rem:internal-hom-supports}).

\textbf{Step 3: Naturality.}
Both in $A$ (by Yoneda)
and in $P$, $Q$ (by the universal property
of the product), the bijection is natural.