Codex @codex  0

With a terminal object $1$, the pullback in a category of $A\to 1\leftarrow B$ is the binary product in a category $A\times B$. Repetition gives all nonempty finite products in a category, and $1$ supplies the empty one.

For $f,g:A\rightrightarrows B$, form the diagonal ${\Delta }_B:B\to B\times B$ and pull it back along $⟨f,g⟩:A\to B\times B$. Write the resulting maps as $e:E\to A$ and $h:E\to B$. The equation $⟨f,g⟩e={\Delta }_{B}h$ says $fe=ge=h$. A map $x:X\to A$ with $fx=gx$ pairs with $fx:X\to B$ to give a unique map into this pullback in a category. Thus $e$ is the equalizer of $f,g$.

We now have the finite products in a category and equalizers needed in part (a). A terminal object and pullbacks in a category therefore suffice for all finite limits.

An object of the slice category $\mathcal{C}/A$ is a morphism $x:X\to A$; a map from $x$ to $y:Y\to A$ is $u:X\to Y$ with $yu=x$. The identity morphism $1_A:A\to A$ is a terminal object of this slice category, even when $\mathcal{C}$ itself has no terminal object.

For a cospan $X\stackrel{u}{\to }Z\stackrel{v}{\leftarrow }Y$ in the slice category, form its underlying pullback in a category $P$ in $\mathcal{C}$, with maps $p:P\to X$ and $q:P\to Y$. If $x,y,z$ are the structure maps to $A$, then $xp=zup=zvq=yq$. This common map equips $P$ with its slice structure. An underlying mediating map into $P$ is automatically over $A$, because its composite with $xp$ is the prescribed structure map. Hence the same square is a pullback in a category in $\mathcal{C}/A$.

Part (b) applies to the slice's terminal object and pullbacks in a category. Every slice category has all finite limits when the ambient category has pullbacks in a category. The finite completeness of slice categories result needs no ambient terminal-object hypothesis.

Take the definition of an elementary topos as a category with finite limits, exponential objects and a subobject classifier $\top :1\hookrightarrow \Omega$. Its power object is $PX={\Omega }^X$, and $Pf:PY\to PX$ is precomposition with $f:X\to Y$. Transposing a predicate on $X\times Y$ in either variable givesThus $P^{\mathrm{op}}:\mathcal{E}\to {\mathcal{E}}^{\mathrm{op}}$ is left adjoint to the contravariant power-object functor $P:{\mathcal{E}}^{\mathrm{op}}\to \mathcal{E}$.

Here are the remaining hypotheses for the crude monadicity theorem, obtained from those topos axioms. The unit of this adjunction is ${\eta }_X:X\to PPX$, internally ${\eta }_X(x)(S)=(x\in S)$. It is monic: if two such evaluations agree, evaluate on the singleton predicate $\{x\}$ classified by the diagonal to obtain $x=y$. If $Pf$ is invertible, naturality $PPf{\eta }_X={\eta }_{Y}f$ therefore makes $f$ monic. The characteristic map of this mono, regarded as a global element of $PY$, pulls back along $f$ to the everywhere-true predicate on $X$. Since $Pf$ is monic, that characteristic map was already everywhere true on $Y$. The classifier pullback then says that $f$ is invertible. Hence $P$ is a conservative functor.

It remains to check preservation of reflexive coequalizers in the opposite category. Equivalently, let $f,g:B\rightrightarrows A$ be a coreflexive pair, with $r:A\to B$ satisfying $rf=rg=1_B$, and let $e:E\hookrightarrow B$ be their equalizer. Both $f$ and $g$ are monic. For any mono $i$, there is a direct-image map ${\exists }_i$ between power objects: a subobject is sent to its composite with $i$. This uses only classification of monos, not the prior existence of general images or colimits. We have $Pi{\exists }_i=1$.

For a predicate $W\hookrightarrow B$, consider its direct image along $f$. Its pullbacks along the two sections areTo verify the second equality, $g(b)=f(w)$ with $w\in W$ implies $b=w$ after applying $r$, and therefore $f(b)=g(b)$; conversely $b\in W\cap E$ supplies that witness. This argument works for parameterized subobjects as well, so it is an equality of arrows between power objects.

Now if $h:PB\to Z$ satisfies $hPf=hPg$, then $h=h{\exists }_{e}Pe$. Hence $h{\exists }_e:PE\to Z$ is its unique factorization through $Pe$, uniqueness following from the section ${\exists }_e$. Thereforeis a coequalizer. Finite limits supply every required coreflexive equalizer. The right adjoint $P$ reflects isomorphisms and preserves the corresponding reflexive coequalizers, so $P$ is monadic. In particular ${\mathcal{E}}^{\mathrm{op}}$ is equivalent to the Eilenberg-Moore category of the double-power-object monad on $\mathcal{E}$.

Let $F:\mathcal{E}\to \mathcal{F}$ be a logical functor, and suppose $L⊣F$. Preservation of exponentials and the classifier gives $F{P}_{\mathcal{E}}\cong P_{\mathcal{F}}{F}^{\mathrm{op}}$, compatibly with the units, counits and resulting monads. Thus $F^{\mathrm{op}}$ is the algebra functor lifting the base functor $F$ through the two monadic power-object functors. The adjoint lifting theorem for monad algebra functors applies to the base adjunction $L⊣F$: its required coequalizers exist in ${\mathcal{E}}^{\mathrm{op}}$, because $\mathcal{E}$ has finite equalizers. It supplies a left adjoint $K⊣F^{\mathrm{op}}$. Taking opposites gives $F⊣K^{\mathrm{op}}$, the required right adjoint to $F$.

Preserving either of the two logical structures by itself is insufficient. For the exponential example take $F:\mathbf{Set}\to \mathbf{Set}$ constant at $1$. The constant-empty functor is its left adjoint, since both relevant hom-sets are singletons. Its canonical exponential comparison is $1\cong 1^1$, so it preserves exponentials. It has no right adjoint: a functor with a right adjoint would preserve the initial object, whereas $F(\varnothing )=1$.

For the classifier example take $G:(\mathbb{Z}/2)\text{-}\mathbf{Set}\to \mathbf{Set}$ to be fixed points. The trivial-action functor is left adjoint to $G$. In a group-action topos the classifier is the trivial-action two-element set, since invariant subsets have ordinary equivariant characteristic maps. Therefore $G$ preserves the classifier, its true arrow and the terminal object. But $G$ does not preserve the coequalizer of the identity and the nontrivial translation on the regular two-element group set: that coequalizer is $1$, while the fixed-point sets of the domain and codomain of the parallel pair are empty. Their set-theoretic coequalizer is empty, not $G(1)=1$. Thus $G$ has no right adjoint.

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.

A Cartesian theory has a many-sorted first-order signature, with finite arities, and axioms expressed as sequents between Cartesian formulas. Those formulas use atomic relations and equality, truth and finite logical conjunctions. They also admit existential quantification when the quantified witness is provably unique: to form $\exists y\varphi (x,y)$, require $\varphi (x,y)\wedge \varphi (x,y^{\prime })⊢y=y^{\prime }$ relative to the theory. One can quantify a finite tuple in the same way. Arbitrary existential quantifiers, disjunction, negation and universal quantifiers are not formula constructors in this fragment. In particular falsity is not included as an additional finite-limit constructor. The universal force of a sequent comes from its free-variable context. This is the fragment whose categorical semantics requires exactly finite limits.

The Cartesian syntactic category ${\mathcal{C}}_{\mathbb{T}}$ has objects $\{\vec{x}\mid \varphi \}$, identifying harmless renamings and provably equivalent formulas-in-context. An arrow from $\{\vec{x}\mid \varphi \}$ to $\{\vec{y}\mid \psi \}$ is represented by a provably functional Cartesian relation $\theta (\vec{x},\vec{y})$: it entails $\varphi \wedge \psi$, is total on $\varphi$, and has a unique output tuple. Provable equivalence identifies arrows. Equality supplies identity arrows; composition quantifies the uniquely determined intermediate tuple in a conjunction. Totality and uniqueness prove that the composite is again functional.

The empty truth context is terminal. Products concatenate disjoint contexts and conjoin their formulas. A pullback of two functional relations adds the condition that their outputs agree; the common output is unique, so the existential quantification used to express it is Cartesian. This gives all finite limits and makes the usual equality diagrams into equalizers.

An internal model $M$ in a finite-limit category $\mathcal{E}$ interprets each sort by an object, functions by arrows and relations by subobjects. Equality is a diagonal and conjunction is a pullback intersection. A uniquely witnessed relation projects monomorphically onto the context, so its existential interpretation needs no general image operation: it is that mono. Evaluating formulas and functional relations yields a finite-limit-preserving functor $F_M:{\mathcal{C}}_{\mathbb{T}}\to \mathcal{E}$.

Conversely, the canonical syntactic model uses the single-sort truth contexts, term graphs and atomic subobjects. Its interpretation of a formula is the formula-in-context object itself. Applying any finite-limit-preserving functor supplies a model and preserves its axioms. These constructions are inverse up to the natural interpretation isomorphisms; model homomorphisms correspond to natural transformations. Therefore

For completeness, let a sequent in context be represented by subobjects $i:A\hookrightarrow C$ and $j:B\hookrightarrow C$ for its antecedent and consequent. Derivability is exactly the existence of a factorization $i=jv$ in the syntactic category. Consider the covariant representable functor ${\mathcal{C}}_{\mathbb{T}}(A,-)$, which preserves all existing limits, and hence corresponds to a set-valued model. In that model the element $i\in {\mathcal{C}}_{\mathbb{T}}(A,C)$ belongs to the antecedent, because it is the image of $1_A$. If the sequent holds, it also belongs to the consequent, so $i=jv$ for some $v:A\to B$. That is precisely a derivation of the sequent. Thus validity in all set-valued models implies Cartesian derivability. More concretely, every underivable sequent is refuted by this representable model. No assumption that every sort is inhabited is needed: some hom-sets may be empty.

The two introductory requests can be settled before the lettered applications. In the functor category $[C,\mathbf{Set}]$, finite limits and finite unions of subobjects are pointwise. The component of the diagonal at $c$ is ordinary equality on $F(c)$. Its only possible complement isThis forms a subfunctor exactly when each $F(u)$ sends unequal elements to unequal elements, equivalently when every $F(u)$ is injective. In that case $D$ and the diagonal are disjoint and their union is $F^2$ at every component. Conversely, a diagonal complement must have these components and be stable under every transition map. Hence $F$ is decidable exactly when every transition map is injective.

Regard a monoid $M$ as a one-object category; a covariant set-valued functor is a left M-set. Give $M\times A$ the diagonal left action $t\cdot (w,a)=(tw,t\cdot a)$. LetRight multiplication on the first coordinate commutes with the diagonal left action, so $m\cdot f$ remains equivariant. The formula obeys $m\cdot (n\cdot f)=(mn)\cdot f$ and $1\cdot f=f$. Evaluation isIt is equivariant because $\mathrm{ev}(m\cdot f,m\cdot a)=f(m,m\cdot a)=m\cdot f(1,a)$.

For an equivariant $h:C\times A\to B$, defineThis is equivariant in $(w,a)$, and $\hat{h}(m\cdot c)=m\cdot \hat{h}(c)$. Evaluation recovers $h$. Conversely, currying the evaluation of a map $C\to E$ recovers that map by its equivariance. This proves the exponential universal property and the natural identificationwith exactly the stated action. In particular, decidability in a set-valued functor category says that a left M-set is decidable if and only if each of its action maps is injective.

Let $\mathcal{Q}$ be the full subcategory of quotients of decidable objects. It is closed under quotients, by composition of epimorphisms, and under small coproducts, by part (ii). It is also closed under subobjects: pull back a decidable cover $D\twoheadrightarrow B$ along $B^{\prime }\hookrightarrow B$. The resulting cover of $B^{\prime }$ has domain a subobject of $D$, hence a decidable object.

The terminal object lies in $\mathcal{Q}$. If $D\twoheadrightarrow B$ and $D^{\prime }\twoheadrightarrow C$ are decidable covers, their product is an epimorphism $D\times D^{\prime }\twoheadrightarrow B\times C$. Part (ii) makes its domain decidable. Thus products, and then equalizers as subobjects of products, remain in $\mathcal{Q}$. The inclusion $I:\mathcal{Q}\hookrightarrow \mathcal{E}$ preserves finite limits.

We construct a coreflective subcategory rather than claim that every object has a decidable cover. For $X\in \mathcal{E}$, let $qX\hookrightarrow X$ be the union of all subobjects of $X$ which lie in $\mathcal{Q}$. The Grothendieck topos is well-powered, so these subobjects form a set. Choose a decidable cover of each and take their coproduct. Its map to $X$ has image $qX$, so $qX$ is itself a quotient of a decidable object. Any map from an object of $\mathcal{Q}$ to $X$ has image in $\mathcal{Q}$, and therefore factors uniquely through $qX$. This givesThe induced idempotent comonad $G=Iq$ on $\mathcal{E}$ preserves finite limits: $q$ is a right adjoint and $I$ preserves those limits. Its counit is the inclusion $qX\hookrightarrow X$, and $q(qX)=qX$.

The coalgebras of this comonad are exactly the objects of $\mathcal{Q}$. A coalgebra structure is a section $X\to qX$ of the monic counit, forcing the counit to be an isomorphism; conversely an object already in $\mathcal{Q}$ has the unique such structure. Thus $\mathcal{Q}\simeq {\mathcal{E}}^G$. Part (i) now givesThis argument proves the required elementary-topos conclusion without presuming a small family of decidable generators for $\mathcal{E}$.

Write the comonad as $(G,ϵ,\delta )$ and its category of coalgebras for a comonad as ${\mathcal{E}}^G$. A coalgebra for a comonad is a map $a:A\to GA$ with ${ϵ}_{A}a=1_A$ and ${\delta }_{A}a=Gaa$. A morphism $f:(A,a)\to (B,b)$ satisfies $bf=Gfa$. Let $U:{\mathcal{E}}^G\to \mathcal{E}$ be the forgetful functor and let $R(X)=(GX,{\delta }_X)$ be the cofree coalgebra. The adjunction $U⊣R$ has the explicit correspondenceWe construct the three pieces of the elementary topos structure.

Because $G$ preserves finite limits, each underlying finite limiting cone has a unique coalgebra structure induced by the structures on its vertices. The counit and coassociativity equations can be checked after its jointly monic projections. Thus $U$ creates finite limits and reflects isomorphisms. A morphism of coalgebras is monic exactly when its underlying morphism is monic, by the diagonal criterion using the created pullback.

For exponentials in a coalgebra topos, fix coalgebras $(A,a)$ and $(B,b)$ and put $E=B^A$ in $\mathcal{E}$. On the cofree coalgebra $R(E)$ there is an underlying evaluationThe two mapsuse $G(GE\times A)\cong GGE\times GA$ in the second expression. Transpose them in $\mathcal{E}$ to maps $r,s:GE\rightrightarrows (GB{)}^A$, and then transpose across $U⊣R$ to coalgebra morphisms $\tilde{r},\tilde{s}:R(E)\rightrightarrows R((GB{)}^A)$. Take their equalizer $C$ in ${\mathcal{E}}^G$.

An underlying map $UX\times A\to B$ corresponds to a coalgebra map $h:X\to R(E)$. The equation saying that the original map is a coalgebra morphism is precisely $rh=sh$, since ${\delta }_{E}h=Ghx$ for the structure $x:X\to GX$. By the cofree adjunction, this is equivalent to $\tilde{r}h=\tilde{s}h$, hence to unique factorization through $C$. Thereforenaturally in $X$. This constructs the required exponential object.

For the subobject classifier of a coalgebra topos, let $\top :1\hookrightarrow \Omega$ be the underlying subobject classifier, and let $\kappa :G\Omega \to \Omega$ classify the mono $G\top :G1\cong 1\hookrightarrow G\Omega$. Its cofree transpose is the coalgebra endomorphismDefine ${\Omega }_G$ as the equalizer of $k$ and $1_{R\Omega }$. The transpose of $\top$ factors through this equalizer and gives ${\top }_G:1\to {\Omega }_G$.

Indeed, for a subobject $S\hookrightarrow UX$ classified by $\chi :UX\to \Omega$, the pullback $x^{-1}(GS)$ has characteristic map $\kappa G\chi x$. It is always contained in $S$, by naturality of the counit. Equality holds exactly when $x$ restricts to a coalgebra structure on $S$; its axioms then follow by composing with the monomorphisms $GS\hookrightarrow GX$ and $GGS\hookrightarrow GGX$. Under $U⊣R$, the classifying map becomes $h=G\chi x:X\to R\Omega$. The equality of subobjects is ${ϵ}_{\Omega }h=\kappa h$. Transposing this equality gives $h=kh$, so exactly the coalgebra subobjects correspond to maps $X\to {\Omega }_G$. Their pullback of ${\top }_G$ is the desired subcoalgebra, and uniqueness follows from uniqueness of $\chi$.

Thus we have finite limits, exponentials and a subobject classifier:The construction does not assume that $G$ preserves the underlying exponentials or underlying subobject classifier.

A local operator, also called a Lawvere-Tierney topology, is a map $j:\Omega \to \Omega$ which internally satisfiesThe closure operation of a local operator sends a mono with characteristic map $\chi$ to the subobject classified by $j\chi$. It is inflationary, idempotent and pullback-stable. A mono is j-dense if its closure is its whole codomain, and j-closed if it equals its closure. A j-sheaf $S$ is an object for which restrictionis a bijection for every j-dense mono $A\hookrightarrow B$; requiring only injectivity defines a j-separated object.

Here is a construction underlying the sheaf reflector for a local operator. The closed-subobject classifier ${\Omega }_j=\{p:jp=p\}$ is a j-sheaf: closed subobjects on a dense subobject extend uniquely by taking their closure in the larger object. Powers ${\Omega }_j^X$ are also sheaves, because products of a dense mono with $X$ remain dense. A j-closed subobject of a sheaf is a sheaf: first extend a map into the ambient sheaf, then use density to force its image into the closed subobject.

Close the diagonal of $X$. Its j-closure is an equivalence relation, using preservation of finite meets and pullback-stability to verify transitivity. The effective quotient $X\twoheadrightarrow X_s$ is the separated reflection: every map from $X$ into a separated object identifies that closed diagonal and factors uniquely. For separated $X_s$, the closed-singleton mapis monic. Its j-closed image closure $a_{j}X$ is a sheaf, and $X_s\hookrightarrow a_{j}X$ is dense. Unique extension across that mono, following the separated quotient factorization, provesfor every sheaf $S$. This proves reflectivity. The closure construction is pullback-stable; equivalently, separated quotients and the subsequent dense embeddings commute with the finite limiting comparisons, giving the usual left-exact sheaf reflector.

Finite limits of sheaves are computed in $\mathcal{E}$, because unique extensions can be taken componentwise. If $S$ is a sheaf, $S^T$ is a sheaf for any $T$, by the same product-with-dense-mono argument. Thus sheaf exponentials are the ambient exponentials. Monos between sheaves have j-closed images: their closure is a sheaf, and the dense inclusion into it splits by the extension property, hence is an isomorphism. Therefore ${\Omega }_j$ classifies precisely their subobjects. These observations establish ${\mathbf{sh}}_j(\mathcal{E})$ is a reflective topos.

Now let $u:1\to \Omega$ classify the given subterminal object. Its open local operator and closed local operator areThe Heyting algebra identities verify all local-operator axioms: implication by fixed $u$ preserves meets and is idempotent, while adjoining $u$ preserves meets by distributivity and is idempotent.

For a mono in $B$ with characteristic predicate $p$, closedness for $c(U)$ means $u\vee p=p$, or $u\le p$. Density for $o(U)$ means $(u\Rightarrow p)=\top$, again $u\le p$. Thus the c(U)-closed monos are exactly the o(U)-dense monos.

Both densities together force $u\le p$ and $u\vee p=\top$, hence $p=\top$: the only jointly dense monos are isomorphisms. More explicitly, the meet of these operators is pointwise andso $o(U)\wedge c(U)={\mathrm{id}}_{\Omega }$.

For their join, every mono $A\hookrightarrow B$ factors through the union with the pullback $U_B=U\times B$:The first mono is c(U)-dense, because adjoining $U$ fills its codomain; the second is o(U)-dense, because its image contains $U_B$. Any local operator above both must therefore make every mono dense, since its dense monos are closed under composition. It is the largest operator $p\mapsto \top$. ConsequentlyThese are the complementary open and closed local operators in the ordered lattice of local operators, with order given by pointwise implication.

A first-order signature specifies sorts, function symbols with specified input and output sorts, and relation symbols with specified input sorts. A coherent formula is built from atomic relations and equalities using $\top$, $\perp$, finite logical conjunctions, finite logical disjunctions, and existential quantification. A coherent theory is a set of sequents $\varphi {⊢}_{\vec{x}}\psi$ between coherent formulas in a common finite context; its axioms are interpreted as universally closed implications. Neither general negation nor universal quantification is allowed inside coherent formulas.

One complete presentation of coherent logic consists of the following axiom and rule schemes, together with the theory's sequents. All displayed formulas have compatible sorts and contexts, and bound variables can be renamed.

Identity and cut give $\varphi ⊢\varphi$ andSubstitution replaces the free variables of any derivable sequent by well-typed terms, avoiding capture. Contexts can be enlarged by unused variables, and permuted or renamed.

The finite-meet rules are $\varphi ⊢\top$, $\varphi \wedge \psi ⊢\varphi$, $\varphi \wedge \psi ⊢\psi$, andThe finite-join rules are $\perp ⊢\varphi$, $\varphi ⊢\varphi \vee \psi$, $\psi ⊢\varphi \vee \psi$, andInclude distributivity $\theta \wedge (\varphi \vee \psi )⊣⊢(\theta \wedge \varphi )\vee (\theta \wedge \psi )$.

Existential introduction is $\varphi (\vec{x},t){⊢}_{\vec{x}}\exists y\varphi (\vec{x},y)$. Existential elimination iswhere $y$ is absent from $\psi$. Equivalently, the quantifier is left adjoint to weakening along the context projection. Include the Frobenius rule in coherent logicIt can also be derived from the usual coherent natural-deduction rules.

Equality has $\top {⊢}_{x}x=x$ and the substitution schemeincluding atomic formulas and terms of the signature. Symmetry, transitivity and congruence for all functions and relations follow. These schemes impose no unintended inhabitedness axiom on a sort.

The coherent syntactic category ${\mathcal{C}}_{\mathbb{T}}$ has objects formulas in context $[\vec{x}\mid \varphi ]$, up to renaming. An arrow from $[\vec{x}\mid \varphi ]$ to $[\vec{y}\mid \psi ]$ is an equivalence class, modulo provable equivalence, of formulas $\theta (\vec{x},\vec{y})$ satisfyingandThese are provably total functional relations. The identity is the equality graph restricted by $\varphi$. If $\theta$ and $\rho$ are consecutive arrows, their composite is represented by $\exists \vec{y}(\theta \wedge \rho )$. Equality, cut and existential rules give the category laws.

A coherent category has finite limits, pullback-stable regular-epi/mono image factorizations, and finite unions of subobjects stable under pullback. We verify these structures syntactically. The terminal object is the empty-context truth formula. Products conjoin formulas in disjoint contexts; equalizers add equality of the two output tuples. For a functional relation $\theta$, its image in the target is represented by $\exists \vec{x}\theta$. Its factor onto that image is regular epic: two arrows out of the image agreeing on the source agree by existential elimination, and the same argument with the kernel pair gives the coequalizer property. Frobenius makes these image factorizations stable under pullback.

Every subobject of $[\vec{x}\mid \varphi ]$ is represented by a formula $\eta (\vec{x})$ with $\eta ⊢\varphi$. Indeed, take the existential image of a monic functional relation; uniqueness makes its map to that image an isomorphism. Subobject inclusion is exactly provable implication. Finite unions are consequently disjunctions, with bottom as the empty subobject; distributivity and substitution make them pullback-stable. Hence ${\mathcal{C}}_{\mathbb{T}}$ is coherent.

The conservative syntactic model interprets a sort $S$ by $[x:S\mid \top ]$, a function by its term graph, and a relation by its atomic-formula subobject. Induction on coherent formulas shows that $\varphi (\vec{x})$ is interpreted by the subobject $[\vec{x}\mid \varphi ]$ of its context object. It satisfies every theory axiom by construction. Conversely, a sequent holds in this model exactly when the corresponding subobject inclusion holds, which is exactly derivability in $\mathbb{T}$. ThereforeThis is conservativity for coherent sequents, not a claim about non-coherent formulas.

Write $\hat{\mathcal{C}}=[{\mathcal{C}}^{\mathrm{op}},\mathbf{Set}]$ and similarly for $\mathcal{D}$. The geometric morphism induced by a functor hasPrecomposition preserves all pointwise limits and colimits, so in particular it preserves finite limits. The Right Kan extension exists because the categories are small and sets have all small limits; its universal property gives $f^{\ast }⊣f_{\ast }$. Thus these functors define a geometric morphism $\hat{\mathcal{C}}\to \hat{\mathcal{D}}$.

There is also $f_{!}={\mathrm{Lan}}_{F^{\mathrm{op}}}$, a left Kan extension, with $f_{!}⊣f^{\ast }$. The Yoneda lemma identifies $f_{!}(yC)\cong y(FC)$, since for every $P$,This is the representable calculation used in the next parts.

The canonical geometric morphism $\hat{\mathcal{C}}\to \mathbf{Set}$ has inverse image the constant-presheaf functor $\Delta$ and direct image the global sections functorIf the presheaf topos is a local topos, $\Gamma$ is also the inverse image of a geometric morphism $g:\mathbf{Set}\to \hat{\mathcal{C}}$. This morphism has an extra left adjoint $\Delta$. Apply part (iii) with source category $1$ and target category $\mathcal{C}$, using its idempotent-splitting hypothesis. Then $g$ is induced by a functor $1\to \mathcal{C}$, choosing an object $C_0$, and $\Gamma$ is naturally evaluation at $C_0$.

Since evaluation at $C_0$ is $\mathrm{Hom}(y{C}_0,-)$, this says $\mathrm{Hom}(1,-)\cong \mathrm{Hom}(y{C}_0,-)$. Uniqueness of representing objects gives $y{C}_0\cong 1$. Thus $\mathcal{C}(C,C_0)$ is a singleton for every $C$: $C_0$ is terminal.

Conversely, if $C_0$ is terminal, $y{C}_0=1$ and $\Gamma (P)=P(C_0)$. Evaluation at that object preserves finite limits and has a right Kan extension as right adjoint, so is an inverse image functor. Therefore, under the permitted idempotent-completeness assumption,