Codex @codex  0

Here Cartesian category means a category with all finite limits. Let $m:Y\hookrightarrow X$ be a monomorphism, and let ${\epsilon }_X\hookrightarrow X\times PX$ be universal membership for a power object $PX$. Pull it back to $Y\times PX$ and then regard the result as a subobject of $X\times PX$. Its unique classifier is an endomorphism $r:PX\to PX$: on a parameterized subobject it intersects with $Y$. Intersecting twice has the same result as intersecting once, so uniqueness of classification gives $r^2=r$.

Take the equalizer $q:Q\hookrightarrow PX$ of $r$ and the identity, and restrict membership to $Y\times Q$. For any subobject $S\hookrightarrow Y\times Z$, its composite with $m\times 1_Z$ is a subobject of $X\times Z$, hence is uniquely classified by $s:Z\to PX$. Since it is contained in $Y\times Z$, its intersection with that subobject changes nothing, so $rs=s$ and $s$ factors uniquely through $Q$. Conversely every map $Z\to Q$ gives the original kind of family by pulling back the restricted membership. These inverse operations givenaturally in $Z$. Thus $Q$ is a power object of a subobject, even if no power objects other than $PX$ were assumed.

Now consider the slice category $\mathcal{E}/A$, which has finite limits formed by ambient pullbacks and has terminal object $1_A:A\to A$. The constant family $A\times X\to A$ has slice power object $A\times PX\to A$: for $Z\to A$,and a classifier $Z\to PX$ is equivalently the map $Z\to A\times PX$ over $A$. Every family $p:X\to A$ is a subobject of this constant family through its monic graph $(p,1_X):X\hookrightarrow A\times X$. Apply the first construction inside the slice. Consequently every slice of a Cartesian category with power objects again has power objects.

Write a coalgebra for a comonad as $(A,a)$ with $a:A\to GA$, ${ϵ}_{A}a=1_A$ and ${\delta }_{A}a=Gaa$. Since the Cartesian comonad $G$ preserves finite limits, the forgetful functor $U:{\mathcal{E}}_G\to \mathcal{E}$ creates them: for an underlying limit $K$ of coalgebras, the maps $K\to A_i\to G{A}_i$ induce a unique $K\to GK$ using $GK\cong {\lim }_{i}G{A}_i$. Its counit and coassociativity equations follow after every limiting projection, which jointly detect equality. The same argument makes the limiting cone universal among coalgebra cones. Thus ${\mathcal{E}}_G$ is a Cartesian category; in particular, the product structure on $A\times B$ is $a\times b$ followed by the comparison $GA\times GB\cong G(A\times B)$.

An exponential object needs more than the underlying ambient $B^A$. The cofree coalgebra functor is $R(D)=(GD,{\delta }_D)$, with adjunctionThe inverse sends $\tilde{h}$ to ${ϵ}_D\tilde{h}$; the comonad laws verify that these are inverse and that $\tilde{h}$ is a coalgebra map.

For $(A,a)$ and $(B,b)$, put $D=B^A$ and $W=(GB{)}^A$ in the ambient Cartesian closed category. Define $p,q:GD\to W$ byand by transposing the compositeto obtain $q$. Their cofree-adjoint transposes are coalgebra mapsTake their coalgebra equalizer $e:H\hookrightarrow R(D)$, which exists by the finite-limit construction.

To verify its universal property, let $h:C\to D$ transpose to $t:C\times A\to B$. Its coalgebra transpose $\tilde{h}=Ghc$ factors through $H$ exactly when $p^{♯}\tilde{h}=q^{♯}\tilde{h}$. By the cofree adjunction, this equality is equivalent to $p\tilde{h}=q\tilde{h}$. The first side is $b^{A}h$, because ${ϵ}_{D}Ghc=h$; transposing the second side gives $Gt$ composed with the product coalgebra structure on $C\times A$. The equality therefore says exactlywith the canonical product comparison understood: precisely the condition that $t$ is a coalgebra map. Thusnaturally in the coalgebra $C$. Its evaluation is ambient evaluation after ${ϵ}_{D}e\times 1_A$, and the preceding condition makes it a coalgebra map. This equalizer is the coalgebra exponential, so the category of coalgebras is cartesian closed. This Cartesian closure for a finite-limit-preserving comonad uses no subobject classifier on $\mathcal{E}$.

Precomposition definesIt preserves finite limits because presheaf limits are pointwise. Its right adjoint is a Right Kan extension; explicitly, for $H\in \hat{\mathbb{C}}$,Precomposition in $d$ supplies the restriction maps. To verify the adjunction, a map $P\circ T^{\mathrm{op}}\to H$ sends $x\in P(d)$ to the natural family taking $h:Tc\to d$ to the image in $H(c)$ of $P(h)x$. Conversely evaluate such a family at $d=Tc$, $h=1_{Tc}$; naturality makes the two constructions inverse. Thus $f^{\ast }⊣f_{\ast }$ and $f^{\ast }$ is left exact, giving the required geometric morphism

Identify the reflective subcategory with its full replete image, writing ${\eta }_X:X\to LX$ for the reflection unit. An object $Z$ is fixed by $L$ exactly when precomposition with every ${\eta }_X$ gives a bijection $\mathcal{E}(LX,Z)\to \mathcal{E}(X,Z)$. One implication is the reflection adjunction; for the other, take $X=Z$ to obtain a retraction of ${\eta }_Z$, and uniqueness of maps into the fixed object $LZ$ makes it a two-sided inverse.

An ambient finite limit of fixed objects has this same property: its hom-sets are limits of the hom-sets of the diagram, and a limit of these bijections is a bijection. Thus the ambient terminal object, products and equalizers are fixed and retain their universal properties in the full subcategory. The reflective subcategory is Cartesian, with finite limits computed in the ambient topos.

A coherent category is a regular category with finite unions of subobjects, including the empty union, stable under pullback. Thus it has finite limits, pullback-stable regular-epimorphism/monomorphism image factorizations, and pullback-stable finite joins in each subobject lattice.

Write $U=A\vee B\hookrightarrow X$ and $C=A\wedge B=A{\times }_{X}B$. Their inclusions give a commutative squareTo establish the pushout property, take arrows $a:A\to Y$, $b:B\to Y$ agreeing on $C$. Regard their graphs as subobjects of $U\times Y$ and form their union $R$. Internally, this relation says that a point of $U$ is related to its $a$-value when it lies in $A$, or to its $b$-value when it lies in $B$.

The relation is total because every point of $U$ belongs to at least one of $A,B$. It is single-valued: two witnesses in the same summand give the same value by functionality of that map; witnesses in different summands have their shared point in $C$, where the two maps agree. By the relation argument proved in Question 7's unheaded continuation, the projection $R\to U$ is both a regular epimorphism and monic, hence an isomorphism. It consequently gives a map $h:U\to Y$ restricting to $a,b$.

For uniqueness, the equalizer of two possible maps contains $A$ and $B$, hence contains their union $U$ and is all of $U$. Thus the square is a pushout, provingThis is the unions of subobjects are pushouts property; it does not assume arbitrary pushouts already exist in a coherent category.

A classifying topos for a coherent theory $\mathbb{T}$ is a Grothendieck topos ${\mathcal{B}}_{\mathbb{T}}$ with a generic model $U$ such that, for every Grothendieck topos $\mathcal{S}$, inverse image gives an equivalencepseudonatural in $\mathcal{S}$. The equivalence includes model homomorphisms and geometric transformations, not merely a bijection between isomorphism classes of set-based models.

Construct the coherent syntactic category ${\mathcal{C}}_{\mathbb{T}}$. Its objects are coherent formulas in finite contexts, modulo provable equivalence, and an arrow is a provably total single-valued coherent relation between their contexts. Composition existentially quantifies the intermediate tuple. Context concatenation, conjunction and equality give finite limits; existential quantification gives stable images; finite disjunction gives stable finite unions. Thus it is a small coherent category, after choosing representatives.

Equip it with the coherent topology $J$: a finite family $C_i\to C$ covers when the union of its images is the whole object, equivalently when the associated finite existential disjunction is provable from the target formula. Pullback stability and closure of covers under composition follow from the corresponding properties of images and unions. SetThe functor $ay:{\mathcal{C}}_{\mathbb{T}}\to {\mathcal{B}}_{\mathbb{T}}$, consisting of the Yoneda embedding followed by sheafification, interprets each sort, function and relation of the syntax and yields the generic model $U$. It preserves finite limits, images and finite unions: syntactic covers become epimorphic families after sheafification, and the syntactic image factorization thus becomes the image factorization of the corresponding arrow. All the axioms consequently hold in $U$.

Here is the classifying argument. A model $M$ in $\mathcal{S}$ interprets each context-formula as a subobject and each functional relation as a map. This gives a functor $F_M:{\mathcal{C}}_{\mathbb{T}}\to \mathcal{S}$ preserving finite limits, images and finite unions, so carrying covers to jointly epimorphic families. Conversely such an interpretation functor recovers exactly a model and all its formula interpretations. Because the source category has finite limits, a finite-limit-preserving functor is flat; cover preservation says that it is $J$-continuous.

For explicitness, the associated inverse image is the flat tensor extensionwhere a set of sections indexes a coproduct and the coend identifies the two actions of every arrow. Flatness makes this extension preserve finite limits. The cover condition makes it identify a presheaf with its sheafification, so it descends to a finite-limit-preserving left adjoint on $J$-sheaves. Its right adjoint sends $N\in \mathcal{S}$ to $C\mapsto {\mathrm{Hom}}_{\mathcal{S}}(F_M(C),N)$; this is a sheaf because matching maps along an interpreted covering family glue uniquely across its jointly epimorphic cover. This is the Diaconescu equivalence for geometric morphisms, with its actual functors displayed.

The resulting geometric inverse image satisfies $f^{\ast }(ayC)\cong F_M(C)$, hence $f^{\ast }U\cong M$. Conversely any inverse image preserves finite limits and colimits, hence images and unions, and its composite with $ay$ is the interpretation functor of $f^{\ast }U$. Since the sheafified representables generate the topos, these constructions recover the geometric morphism up to its unique appropriate isomorphism. Natural transformations of interpretation functors correspond to the model homomorphisms and geometric transformations. This proves the required equivalence and the construction's classifying property.

Write $\hat{\mathcal{C}}=[{\mathcal{C}}^{\mathrm{op}},\mathbf{Set}]$ and similarly for $\mathcal{D}$. The induced inverse-image functor is precomposition:All categorical limits in a presheaf category are computed pointwise. Thus $u^{\ast }$ preserves every limit, in particular finite limits.

Because the indexing categories are small and $\mathbf{Set}$ is complete and cocomplete, both Kan extensions along $f^{\mathrm{op}}$ exist. Their universal properties giveFor example their values are the comma-category formulasThe comma categories here are formed in ${\mathcal{D}}^{\mathrm{op}}$: an object of the first involves $f(c)\to d$ there, equivalently $d\to f(c)$ in $\mathcal{D}$. An object of the second involves $d\to f(c)$ there, equivalently $f(c)\to d$ in $\mathcal{D}$. Keeping the opposite category explicit prevents reversal of the two constructions.

The right-hand adjunction and finite-limit preservation are exactly the axioms for a geometric morphism $u:\hat{\mathcal{C}}\to \hat{\mathcal{D}}$. The extra left adjoint makes it an essential geometric morphism. On representable presheaves, its left adjoint satisfies $u_{!}(y_{\mathcal{C}}c)\cong y_{\mathcal{D}}(fc)$, by the Yoneda lemma and the left adjunction. This identifies the induced morphism directly with the original functor $f$.

Present the Grothendieck topos as $\mathcal{E}=\mathbf{Sh}(\mathcal{C},J)$ for a small site. Let $a:\hat{\mathcal{C}}\to \mathcal{E}$ be sheafification and $i$ the inclusion. The standard sheafification construction supplies $a⊣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 exponentialIt is a sheaf. Indeed, for a covering sieve $S\hookrightarrow yc$, one has $aS\cong a(yc)$. Exponential adjunction, sheafification adjunction and left exactness giveThese 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^{\ast }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)$ toThis 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. 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:The top is $B$. Arbitrary joins are local unions: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: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 adjunctionFor 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\Rightarrow 0$. These formulas give the complete Heyting algebra structure on ${\mathrm{Sub}}_{\mathcal{E}}(B)$; in general negation is a pseudocomplement rather than a set-theoretic complement.

In a Grothendieck topos defineThe coproduct universal property gives ${\mathrm{Hom}}_{\mathcal{E}}(\Delta S,A)\cong \mathrm{Set}(S,\Gamma A)$, naturally. Thus $\Delta ⊣\Gamma$. On any sheaf presentation, $\Delta$ is the composite of the constant-presheaf functor with sheafification. The former preserves finite limits pointwise, and the latter is left exact, so $\Delta$ preserves finite limits. Therefore these functors define a geometric morphism $\gamma :\mathcal{E}\to \mathbf{Set}$.

For uniqueness, let $v$ be any such geometric morphism. Its inverse image is a left adjoint and preserves the terminal object. Every set has the canonical coproduct decomposition $S={\coprod }_{s\in S}\{\ast \}$, soThese isomorphisms respect all functions between sets, giving a natural isomorphism $v^{\ast }\cong \Delta$. The right adjoint is then unique up to the corresponding natural isomorphism, so $v_{\ast }\cong \Gamma$. There is a unique geometric morphism to sets, up to isomorphism, called the global sections geometric morphism. This also applies to the degenerate topos.

For the covariant category in this part, put $\mathcal{E}=[\mathcal{C},\mathbf{Set}]$ and $r_c=\mathcal{C}(c,-)$. Its global-sections functor is $\Gamma =\mathrm{Hom}(1,-)$, the limit of the diagram. If $\Gamma$ is also an inverse image, it is a left adjoint and preserves all small colimits.

Consider the canonical pointwise-surjective mapAt $d$, the summand $r_d(d)$ contains $1_d$, so $q$ is an epimorphism. In a presheaf topos epimorphisms are regular, and a colimit-preserving functor preserves their coequalizer presentations. Thus $\Gamma q$ is surjective. Since $\Gamma$ preserves coproducts, some summand has a global element, yielding a section $s:1\to r_c$ of its unique map $r_c\to 1$. The constant singleton functor is a retract of a covariant representable.

Conversely, if $1$ is such a retract in a category, $\mathrm{Hom}(1,-)$ is a retract of $\mathrm{Hom}(r_c,-)$, which is evaluation at $c$ by the Yoneda lemma. Evaluation preserves colimits pointwise. The colimit comparison for a retract functor is a retract of the evaluation comparison; a retract of an isomorphism is an isomorphism, so $\Gamma$ preserves all small colimits. It also preserves finite limits because it is representable. A right adjoint can be constructed byFor $h:d\to d^{\prime }$, precomposition gives $r_{d^{\prime }}\to r_d$, and applying $\Gamma$ and then $\mathrm{Set}(-,S)$ gives $R(S)(d)\to R(S)(d^{\prime })$. The presentation of every functor as a colimit of representables gives $\mathrm{Hom}(F,R(S))\cong \mathrm{Set}(\Gamma F,S)$. Hence $\Gamma ⊣R$, so $\Gamma$ is an inverse image and the topos is local.

The retract condition has a precise interpretation as the initial object criterion for a covariant local topos. Write the section as a natural family $u_d:c\to d$. Naturality says $h{u}_d=u_{d^{\prime }}$ for every $h:d\to d^{\prime }$. Put $e=u_c$. Then $e^2=e$ and every $f:c\to d$ satisfies $fe=u_d$. In the idempotent completion of $\mathcal{C}$, the object $(c,e)$ is initial: an arrow from it to $(d,k)$ must satisfy $v=kve$, and the identities force $v=u_d$; this arrow exists because $k{u}_d=u_d$ and $u_{d}e=u_d$.

Conversely an initial object $(c,e)$ in the idempotent completion gives that natural family and the retract. ThereforeIf $\mathcal{C}$ is already idempotent-complete, this is equivalent to an initial object in $\mathcal{C}$ itself, and $\Gamma$ is evaluation there. The word is initial, not terminal, because this question uses covariant functors.

One cannot omit idempotent completion for a general small category. Take the one-object category of the monoid $\{1,0\}$ with absorbing zero. It has no initial object because its endomorphism set has two elements, but the natural family $u=0$ satisfies $m0=0$ for every $m$. Its covariant functor category is local. Concretely, a functor is a set with an idempotent operator, and its global sections are the fixed points of that operator.

For a topological space $X$, there is an equally explicit criterion. If $\mathbf{Sh}(X)$ is local, apply $\Gamma$ to the epimorphism ${\coprod }_i{U}_i\to 1$ associated with any open cover $X={\bigcup }_i{U}_i$, regarding the opens as subterminal sheaves. Since $\Gamma U_i$ is a singleton exactly when $U_i=X$, and otherwise empty, coproduct and epimorphism preservation force some $U_i=X$.

Thus every open cover of $X$ contains $X$ itself. Conversely this open cover criterion for a local sheaf topos condition is equivalent to existence of a point $x$ whose only open neighborhood is $X$: the union of all proper open sets cannot be all of $X$, so choose $x$ outside it. Such a point plainly forces any cover to contain $X$. Empty spaces fail the condition.

At this point, the stalk functor $F\mapsto F_x$ is simply $F(X)=\Gamma F$, since there is only one open neighborhood. Its right adjoint is the skyscraper sheaf of setsA morphism $F\to R(S)$ is determined exactly by its map $F(X)\to S$, because all proper opens omit $x$. Hence $\Gamma ⊣R$, and $\Gamma$ preserves finite limits, proving locality. ConsequentlyIn a $T_0$ space this distinguished point is unique and closed. In a $T_1$ space the condition forces $X$ to be a singleton. Indistinguishable points in a non-$T_0$ space can all have this property; uniqueness of an actual point is not part of the general criterion.

A geometric formula is built from atomic formulas, including equality, using finite conjunctions, arbitrary set-indexed disjunctions and existential quantification in a finite variable context. Truth is the empty conjunction and falsity the empty disjunction. A geometric theory is a set of sequents $\varphi {⊢}_{\vec{x}}\psi$ between such formulas over a many-sorted signature. The context supplies the universal force of an axiom; unrestricted universal quantification, implication and negation are not formula constructors in this fragment.

These choices are exactly suited to inverse image functors of geometric morphisms. Finite-limit preservation handles equality and conjunction; colimit and image preservation handle disjunction and existential quantification. Therefore an inverse image carries an internal model of a geometric theory to another model.

Construct the geometric syntactic category ${\mathcal{C}}_{\mathbb{T}}$ as follows. Objects are formulas in context $\{\vec{x}.\varphi \}$, modulo provable renaming and equivalence. A morphism to $\{\vec{y}.\psi \}$ is an equivalence class of formulas $\theta (\vec{x},\vec{y})$ that are provably total and single-valued:The last notation abbreviates componentwise equality. Identity is equality of the context variables; composition is existential conjunction over the intermediate tuple. The category has finite limits, formed through conjunction and equality.

Give it the geometric syntactic topology $J_{\mathbb{T}}$. A family of arrows represented by ${\theta }_i({\vec{y}}_i,\vec{x})$ into $\{\vec{x}.\varphi \}$ covers whenPullback stability is substitution, and transitivity comes from distributing existential conjunction through the covering disjunctions. Thus the generated sieves define a Grothendieck topology. Empty covers impose the interpretation of falsity as the initial object.

The classifying topos isIts universal model $U_{\mathbb{T}}$ assigns a sort $A$ the sheafified representable of $\{x^A.\top \}$, functions their definable graph morphisms and relations their definable subobjects. The syntactic covering conditions make the axioms valid in this model.

For the universal property, interpreting formulas in a model $M$ in a Grothendieck topos $\mathcal{F}$ gives a finite-limit-preserving, $J_{\mathbb{T}}$-continuous functor ${\mathcal{C}}_{\mathbb{T}}\to \mathcal{F}$: covers go to jointly epimorphic families precisely because the relevant sequents hold. The Diaconescu equivalence for geometric morphisms associates to this functor a geometric morphism $\mathcal{F}\to \mathbf{Set}[\mathbb{T}]$. Conversely, pulling $U_{\mathbb{T}}$ back along a geometric morphism gives a model. The constructions on models and their homomorphisms are inverse up to natural isomorphism, yieldingnaturally in $\mathcal{F}$. This proves the required classifying property, not merely classification of set-valued models.

Yes, with the Horn/Cartesian-fragment convention. A Horn theory uses positive finite-conjunction sequents and has a Cartesian syntactic category ${\mathcal{C}}_{\mathbb{T}}^{\mathrm{cart}}$ with finite limits. Provably uniquely witnessed existential formulas can also be admitted without changing the finite-limit nature of its semantics. Its internal models are precisely finite-limit-preserving functors from that category.

For a category with finite limits, flat functors into a Grothendieck topos are exactly finite-limit-preserving functors. In sets, the reason is concrete: the category of elements of a covariant left-exact functor is cofiltered. Its terminal object supplies nonemptiness, products supply cones over pairs of elements, and equalizers supply equalizing cones over parallel arrows. Conversely a cofiltered category of elements expresses the functor as a filtered colimit of covariant representables; filtered colimits of sets commute with finite limits. The internal version uses the same cone conditions locally.

The presheaf form of the Diaconescu equivalence for geometric morphisms therefore identifies geometric morphisms intowith internal Horn models, naturally in the domain topos. This is the presheaf classifier of a Horn theory.

Equivalently, using a small skeleton of the category $\mathcal{A}$ of finitely presented set-based Horn models, the classifier is $[\mathcal{A},\mathbf{Set}]$, with covariant functors. The duality $\mathcal{A}\simeq ({\mathcal{C}}_{\mathbb{T}}^{\mathrm{cart}}{)}^{\mathrm{op}}$ sends a formula to the model generated by its tuple subject to its finite constraints. The presheaf claim does not extend merely because a general geometric or regular theory has no written disjunctions: arbitrary existential witnesses are not uniquely witnessed Horn data.

Let $D:J\to \mathcal{C}$ be a finite diagram in a category. Form the finite products in a categoryDefine $s,t:P\rightrightarrows Q$ by ${\pi }_{a}s=D(a){\pi }_j$ and ${\pi }_{a}t={\pi }_k$. Take their equalizer $e:L\to P$. The maps ${\lambda }_j={\pi }_{j}e$ satisfy $D(a){\lambda }_j={\lambda }_k$, so they constitute a categorical cone.

Any other categorical cone $x_j:X\to D(j)$ gives a unique $x:X\to P$ by the product in a category property. Its cone equations say $sx=tx$, so the equalizer gives a unique $\bar{x}:X\to L$ with $e\bar{x}=x$. The projections then give ${\lambda }_j\bar{x}=x_j$, and uniqueness follows from both universal properties. Thus this equalizer of two product maps is the finite limit of the diagram in a category.

The empty indexing category is included: its empty product in a category is a terminal object, which is the empty categorical limit. Hence no nonemptiness restriction has entered the construction.