In Lawvere's paper on Elementary Theory of Category of Sets (https://artscimedia.case.edu/wp-content/uploads/2013/07/14182623/Lawvere-ETCS.pdf), at page 27, he proves Lemma 3. by constructing a morphism. For $h:R \to A$, he constructs $\overline{h}:2^R \to 2^A$.
What he does is construct an equalizer $\Psi$ of $R \times 2^R \xrightarrow{\text{eval}} 2$ with $R \times 2^R \to 1 \xrightarrow{i_1} 2$ (I assume $i_1$ plays a role of morphism $\text{true}:1 \to 2$). Afterwards, he composes $\Psi$ with $h \times 2^R$ and taking an image, hence getting a subobject $\text{im} \hookrightarrow A \times 2^R$. Then he takes characteristic function (which I assume is the unique morphism from the definition of subobject classifier), and exponentially transposes it to get $\overline{h}:2^R \to 2^A$.
On the next page, he remarks that we have constructed a covariant direct image functor. I've tried to prove this is a functor, but I couldn't do it.
I've tried proving it for identities ($h = \text{id}_R$), I've concluded that since we are looking at an equalizer, it is a monomorphism, and we compose it with an identity times identity, so the resulting morphism is $\Psi$ itself. Image of a mono is its domain and I use subobject classifier to get $\chi_\Psi$ and transpose it into $\overline{\text{id}_R} := \lambda \chi_\Psi:2^R \to 2^R$. But I don't know how to prove it is equal to $\text{id}_{2^R}$.
As for the composition, I assume I need to prove $\lambda \chi_g \lambda \chi_f = \lambda \chi_{gf}$, but I got nowhere after I constructed $x$ such that $\lambda x = \lambda \chi_g \lambda \chi_f$.
Best Answer
$\require{AMScd}$ First of all, from the role of $2^A$ as a power object of $A$, we can see that for $h : R \to A$, then $\bar h : 2^R \to 2^A$ is the unique morphism such that we have a cartesian square $$\begin{CD} i_h @>>> {\in}_A \\ @V \operatorname{inc}VV @VV \operatorname{inc} V \\ A \times 2^R @> \operatorname{id} \times \bar h >> A \times 2^A \end{CD}$$ where $i_h$ is the image of ${\in}_R \overset{\operatorname{inc}}\to R \times 2^R \overset{h \times \operatorname{id}}\longrightarrow A \times 2^R$. (Here ${\in}_A$ is the subobject of $A \times 2^A$ with characteristic function $\operatorname{eval}_{A, 2}$ and similarly for ${\in}_R$.) Furthermore, using the characterization of image in terms of epi-mono factorization, we see that $\bar h$ is the unique morphism such that we have a commutative diagram $$\begin{CD} {\in}_R @>>> i_h @>>> {\in}_A \\ @V \operatorname{inc} VV @VVV @VV \operatorname{inc}V \\ R \times 2^R @> h \times \operatorname{id} >> A \times 2^R @> \operatorname{id} \times \bar h >> A \times 2^A \end{CD}$$ where the morphism ${\in}_R \to i_h$ is an epimorphism and the right square is cartesian. (Note that the commutativity of the outer rectangle is related to the fact that if $x \in S \subseteq R$, then $h(x) \in \bar h(S)$.)
This immediately gives the identity condition: for any object $A$, we clearly have such a commutative diagram $$\begin{CD} {\in}_A @>>> {\in}_A @>>> {\in}_A \\ @VVV @VVV @VVV \\ A \times 2^A @> \operatorname{id} \times \operatorname{id} >> A \times 2^A @> \operatorname{id} \times \operatorname{id} >> A \times 2^A. \end{CD}$$
Now for the composition condition, suppose we have $g : A \to B$ and $f : B \to C$. Then putting together the above diagrams for $f$ and $g$, we have a commutative diagram $$\begin{CD} {\in}_A @>>> i_g @>>> {\in}_B @>>> i_f @>>> {\in}_C \\ @VVV @VVV @VVV @VVV @VVV \\ A \times 2^A @> g\times\operatorname{id} >> B \times 2^A @> \operatorname{id}\times \bar g >> B \times 2^B @> f\times\operatorname{id} >> C \times 2^B @> \operatorname{id}\times \bar f >> C \times 2^C \end{CD}$$ where the second and fourth squares are cartesian, and the first and third morphisms in the top row are epimorphisms.
Now, considering where we want to end up, let us refactor $(f \times \operatorname{id}) \circ (\operatorname{id} \times \bar g) = (f, \bar g) = (\operatorname{id}, \bar g) \circ (f, \operatorname{id})$, and in the top row, fill in an object constructed to make a second cartesian square. In this way, we get a commutative diagram $$\begin{CD} {\in}_A @>>> i_g @>>> (\operatorname{id} \times \bar g)^* i_f @>>> i_f @>>> {\in}_C \\ @VVV @VVV @VVV @VVV @VVV \\ A \times 2^A @> g\times\operatorname{id} >> B \times 2^A @> f\times\operatorname{id} >> C \times 2^A @> \operatorname{id}\times \bar g >> C \times 2^B @> \operatorname{id}\times \bar f >> C \times 2^C \end{CD}$$ where the right two squares are cartesian, and ${\in}_A \to i_g$ is an epimorphism.
We claim that in fact, the second morphism on the top row, $i_g \to (\operatorname{id} \times \bar g)^* i_f$, is also an epimorphism. To show this, we will show that the commutative square $$\begin{CD} i_g @>>> (\operatorname{id} \times \bar g)^* i_f \\ @VVV @VVV \\ {\in}_B @>>> i_f \end{CD}$$ is cartesian, and then use the fact that ${\in}_B \to i_f$ is an epimorphism. To see this, extend the square above to the commutative diagram $$\begin{CD} i_g @>>> (\operatorname{id} \times \bar g)^* i_f @>>> C \times 2^A \\ @VVV @VVV @VVV \\ {\in}_B @>>> i_f @>>> C \times 2^B. \end{CD}$$ Here, we know that the right square is cartesian; therefore, to show the left square is cartesian, it will suffice to show the composed rectangle is a cartesian square. However, that rectangle can be refactored as $$\begin{CD} i_g @>>> B \times 2^A @> f\times\operatorname{id} >> C \times 2^A \\ @VVV @V \operatorname{id}\times\bar g VV @VV \operatorname{id}\times\bar g V \\ {\in}_B @>>> B \times 2^B @> f\times\operatorname{id} >> C \times 2^B. \end{CD}$$ Here, we know that the left square is cartesian by assumption; and it should be a straightforward exercise to show that the right square is cartesian. Therefore, the outer rectangle is also a cartesian square, completing the proof that $i_g \to (\operatorname{id} \times \bar g)^* i_f$ is an epimorphism.
Now, combining the two left squares, and the two right squares, we get a commutative diagram $$\begin{CD} {\in}_A @>>> (\operatorname{id} \times \bar g)^* i_f @>>> {\in}_C \\ @VVV @VVV @VVV \\ A \times 2^A @> (f\circ g) \times \operatorname{id} >> C \times 2^A @> \operatorname{id} \times (\bar f\circ\bar g) >> C \times 2^C \end{CD}$$ in which the morphism ${\in}_A \to (\operatorname{id} \times \bar g)^* i_f$ is a composition of two epimorphisms, so it is an epimorphism; and the right-hand square is a composition of two cartesian squares, so it is a cartesian square. Therefore, by the uniqueness condition above, we can conclude $\overline{f\circ g} = \bar f \circ \bar g$.
(Note that the proof also gives that $i_{f\circ g} = (\operatorname{id} \times \bar g)^* i_f$ as subobjects of $C\times 2^A$. It might be an interesting exercise to show why this is true in $\mathsf{Set}$.)
Also, note that nothing here used any of the special axioms of ETCS, except for $2$ being the subobject classifier; therefore, the proof above will work for any topos if you just replace $2$ with $\Omega$ throughout.