Solution (source code)

= Solution

Present the <Grothendieck topos> as $\mathcal E=\mathbf{Sh}(\mathcal C,J)$ for a small <site>. Let $a:\widehat{\mathcal C}\to\mathcal E$ be <sheafification> and $i$ the inclusion. The standard <sheafification> construction supplies $a\dashv i$, with $a$ preserving <finite limits>. Concretely, matching-family constructions commute with <finite limits>, and their directed refinement over covering sieves does so as well. Limits of sheaves are computed in the <presheaf category>, so $\mathcal E$ has <finite limits>; its <colimits> are sheafifications of presheaf <colimits>.

For sheaves $A,B$, form the presheaf exponential
$$
E(c)=\operatorname{Nat}(y c\times A,B).
$$
It is a sheaf. Indeed, for a covering sieve $S\hookrightarrow y c$, one has $aS\cong a(y c)$. Exponential <adjunction>, <sheafification> <adjunction> and left exactness give
$$
\operatorname{Nat}(S,E)
\cong\operatorname{Nat}(S\times A,B)
\cong\operatorname{Hom}_{\mathcal E}(aS\times A,B)
\cong\operatorname{Hom}_{\mathcal E}(a(y c)\times A,B)
\cong\operatorname{Nat}(y c,E).
$$
These are the restriction comparisons, proving the sheaf condition. Restricting the presheaf exponential <adjunction> to sheaves now makes $E=B^A$ in $\mathcal E$.

The <subobject classifier> is the sheaf $\Omega_J$ of <J-closed sieves>. A sieve $S$ on $c$ is J-closed when, for every $f:d\to c$, $f^*S\in J(d)$ implies $f\in S$. Pullback of sieves defines its restrictions, and the maximal sieve defines truth. Local sieve data glue by taking the J-closure of their compatible generated sieve; uniqueness follows because membership in a J-closed sieve is local. This proves that $\Omega_J$ is a sheaf.

For a subsheaf $A\hookrightarrow B$, the characteristic morphism sends $b\in B(c)$ to
$$
\chi_A(b)=\{f:d\to c:B(f)(b)\in A(d)\}.
$$
This sieve is J-closed because local membership in a subsheaf descends by its gluing axiom. Pulling truth back recovers exactly $A$. Conversely, pulling back truth along any morphism into $\Omega_J$ gives a subsheaf, and the same formula recovers that morphism. \b[<Finite limits>, exponentials and this classifier make every <Grothendieck topos> an <elementary topos>.]

Here are the explicit <Heyting operations on subsheaves> of an object $B$. Intersections give meets:
$$
(A\wedge D)(c)=A(c)\cap D(c),\qquad
\left(\bigwedge_i A_i\right)(c)=\bigcap_i A_i(c).
$$
The top is $B$. Arbitrary joins are local unions:
$$
\boxed{
b\in\left(\bigvee_iA_i\right)(c)
\ \Longleftrightarrow\
\{f:d\to c:B(f)b\in A_i(d)\text{ for some }i\}\in J(c).}
$$
Equivalently, $b$ locally lies in one of the $A_i$, with the index allowed to vary across the covering arrows. This is the J-closure of the pointwise union, or its <sheafification>. It is the smallest subsheaf containing every $A_i$, since any such subsheaf must contain sections locally in it.

The bottom is the empty join, namely the initial <subobject>. Its value at $c$ consists of all $b\in B(c)$ if the empty sieve covers $c$, and is empty otherwise. This detail matters on <sites> with empty covers; it is not safe to use an always-empty presheaf as the initial sheaf.

Implication is described without any pointwise-complement assumption:
$$
\boxed{
(A\Rightarrow D)(c)=
\{b\in B(c):
\text{ for every }f:d\to c,\ B(f)b\in A(d)\Longrightarrow B(f)b\in D(d)\}.}
$$
Restrictions preserve this condition. It is also local: pull a covering sieve back along an arbitrary $f$, use membership in $A$ on those restrictions, then descend their membership in $D$. Thus it is a subsheaf. It satisfies the defining <Heyting algebra> <adjunction>
$$
C\leq(A\Rightarrow D)\quad\Longleftrightarrow\quad C\cap A\leq D.
$$
For the forward direction take the identity restriction. For the reverse direction every restriction of a section of $C$ remains in $C$, so membership in $A$ forces membership in $D$. Negation is $\neg A=A\Rightarrow0$. These formulas give the complete Heyting algebra structure on $\operatorname{Sub}_{\mathcal E}(B)$; in general negation is a pseudocomplement rather than a set-theoretic complement.