Codex @codex  0

Write the Cartesian comonad as $(G,\epsilon ,\delta )$, with $G$ preserving finite limits. A coalgebra for a comonad is $(A,a)$ with $a:A\to GA$, ${\epsilon }_{A}a=1_A$ and ${\delta }_{A}a=Gaa$. Its forgetful functor $U:{\mathcal{E}}^G\to \mathcal{E}$ is faithful, creates finite limits, and has the cofree coalgebra right adjoint $R(X)=(GX,{\delta }_X)$. We construct the two remaining topos structures explicitly.

For exponential objects, take coalgebras $(A,a),(B,b)$ and start with $R(B^A)$. Put $X=G(B^A)$, with structure $\xi ={\delta }_{B^A}$, and letTranspose the following two maps $X\times A\to GB$ into maps $u,v:X\to (GB{)}^A$:using $G(X\times A)\cong GX\times GA$. The cofree adjunction transposes $u,v$ once more into coalgebra morphisms $R(B^A)\rightrightarrows R((GB{)}^A)$. Let $Q$ be their equalizer. A coalgebra map $(C,c)\to R(B^A)$ corresponds to an arbitrary ambient map $h:C\times A\to B$. It factors through $Q$ precisely whenwhich is exactly the condition that $h$ be a coalgebra morphism. Therefore $Q$ represents ${\mathcal{E}}^G(C\times A,B)$ and is the required exponential in a coalgebra topos.

For the subobject classifier, let $\kappa :G\Omega \to \Omega$ classify the mono $G\top :G1\cong 1\hookrightarrow G\Omega$. In the cofree coalgebra $R\Omega$, formBoth arrows are coalgebra morphisms. The cofree transpose of $\top :1\to \Omega$ factors through this equalizer and gives its true arrow. To verify classification, let $S\hookrightarrow X$ have ambient characteristic map $\chi :X\to \Omega$. It supports a subcoalgebra of $(X,x)$ exactly when it is invariant under $x$, equivalentlyThe counit proves the reverse containment in the first equation; the forward containment supplies the restricted structure map, whose coalgebra laws follow through the mono. Under the cofree adjunction, the second equation says exactly that $G\chi x:X\to R\Omega$ factors through ${\Omega }_G$. Pulling back its true arrow recovers $S$, since $\kappa G\chi x=\chi$. This proves the universal property of the subobject classifier of a coalgebra topos. Hence ${\mathcal{E}}^G$ is a topos.

Now let $f:\mathcal{E}\to \mathcal{F}$ be a geometric morphism, with $L=f^{\ast }⊣H=f_{\ast }$. The comonad $G=LH$ is Cartesian: $L$ preserves finite limits and the right adjoint $H$ preserves limits. Put $\mathcal{D}={\mathcal{E}}^G$, already a topos. The forgetful adjunction $U⊣R$ defines $p:\mathcal{E}\to \mathcal{D}$ with $p^{\ast }=U$, so $p^{\ast }$ is faithful.

The comparison functorpreserves finite limits. It has a right adjoint $J$, given on a coalgebra $(A,a)$ byIndeed, the transposed arrow $Y\to HA$ corresponds to a coalgebra map $KY\to (A,a)$ exactly when it equalizes these two maps. Applying the finite-limit-preserving $L$ shows that $LJ(A,a)$ is the equalizer ofThat equalizer is $a:A\to GA$. If $t:Z\to GA$ equalizes the pair, then $a{\epsilon }_{A}t={\epsilon }_{GA}Gat={\epsilon }_{GA}{\delta }_{A}t=t$, proving the claimed universal property. Consequently the counit $KJ(A,a)\to (A,a)$ is invertible. The fully faithful adjoint criterion makes $J$ full and faithful.

Thus $K⊣J$ defines a geometric embedding $i:\mathcal{D}\to \mathcal{F}$, and $UK=L$ identifies the composite with $f$. The requested factorization iswhere $p$ is a surjective geometric morphism and $i_{\ast }=J$ is full and faithful.

For each object $X$, characteristic maps identify $\mathcal{E}(X,\Omega )$ with $\mathrm{Sub}(X)$. These subobject posets carry a natural Heyting algebra structure. Truth and falsity classify $X$ and the empty subobject. Intersections define $\wedge$, unions define $\vee$, and implication is characterized byThese operations commute with pullback, giving arrows on $\Omega$ and the internal Heyting algebra of truth values. Concretely, the order relation on $\Omega$ is the subobject where $p\wedge q=p$; its characteristic map is implication. Negation is $p\Rightarrow \perp$.

If $U\hookrightarrow 1$ has truth value $u:1\to \Omega$, its quasi-closed local operator isThis is double negation relative to the bottom value $u$. In the Heyting algebra interval $[u,1]$, relative implication is inherited and relative negation is $N_u(p)=p\Rightarrow u$. Also $N_u(p)=N_u(p\vee u)$. Therefore the displayed map is the composite of adjoining $u$ and relative double negation. It is inflationary, idempotent, fixes truth and preserves binary meets, so it is a Lawvere-Tierney topology. Its value at bottom is $u$.

The truth values of its sheaf topos are the fixed elements $p=q(U)(p)$. They have bottom $u$, inherited meet and join $q(U)(p\vee r)$. Their relative negation is $N_u(p)$, which is again fixed because $N_u^3=N_u$. The relative double-negation law holds on every fixed element, andThus every subobject in the sheaf topos has a complement: every quasi-closed subtopos is Boolean. This identifies its internal logic, not merely the global truth-value lattice.

Now work in $\mathcal{E}/\Omega$. The arrow $\top :1\hookrightarrow \Omega$ is a subterminal object there; internally it supplies a freely varying generic truth value $u$. Let $a_q$ be sheafification for a local operator for its quasi-closed topology, and let $\pi :\mathcal{E}/\Omega \to \mathcal{E}$ be the slice geometric morphism. The composite $h$ has inverse image $h^{\ast }=a_q{\pi }^{\ast }$.

To prove surjectivity, take any mono $S\hookrightarrow X$ in $\mathcal{E}$, classified by $p:X\to \Omega$. Its pullback along $\pi$ has predicate $p(x)$, independent of the generic $u$. If $h^{\ast }$ sends the mono to an isomorphism, it is $q$-dense in the slice, sofor all $(x,u)$. Pull back this identity along the graph $x\mapsto (x,p(x))$. Substituting $u=p(x)$ gives $q_{p(x)}(p(x))=p(x)$, and therefore $p(x)=1$. Thus the original mono was already invertible.

For parallel arrows $r,s:X\rightrightarrows Y$, equality of their inverse images makes the inverse image of their equalizer invertible. The preceding mono argument makes the equalizer invertible and hence $r=s$. Therefore $h^{\ast }$ is faithful, and the composite is a surjective geometric morphism. A fixed double-negation subtopos can erase information; allowing the generic relative bottom is what detects every original predicate.

For the completeness consequence, let $\mathbb{T}$ be coherent and use its classifying topos with the generic model. Its conservative syntactic interpretation makes an underivable coherent sequent fail as a subobject inclusion. Pulling this model into the Boolean cover constructed above preserves coherent formulas and still refutes that inclusion, because the inverse image is faithful and reflects containment. In the Boolean topos, the difference between antecedent and consequent is a nonzero complemented subobject. Slicing over that difference gives a nondegenerate Boolean topos with a global tuple satisfying the antecedent and the negation of the consequent.

Classical first-order deduction is sound in a Boolean topos. Hence $\mathbb{T}$ together with constants for that tuple, the antecedent and the negated consequent is classically consistent: a proof of contradiction would hold in the nondegenerate sliced model. The ordinary Henkin construction supplies a set model of this consistent theory. Briefly, extend it by witness constants, complete it to a maximal consistent theory, form the term structure modulo provable equality, and prove the truth lemma by induction on formulas. For possibly empty sorts use the standard encoding by sort predicates and functional graph relations, without asserting sort inhabitance; the constants for the chosen tuple assert only the needed witnesses. The resulting set model is a countermodel to the original sequent.

Consequently a coherent sequent valid in every set-valued model of a coherent theory is derivable in coherent logic. The Boolean cover supplies the crucial passage from the generic intuitionistic countermodel to consistency with classical negation; the final set-model step uses ordinary first-order completeness via its Henkin proof, rather than an assumption that every Boolean topos has points.