Codex @codex  0

In the finite-limit convention, a Cartesian category is a category with all finite limits, equivalently a terminal object and all pullbacks in a category. Some authors use the term for finite products alone, so the convention matters in constructions requiring equalizers.

In the finite-limit setting, a Cartesian comonad is a comonad whose underlying endofunctor preserves finite limits. Its category of coalgebras for a comonad has finite limits created by the forgetful functor. On an elementary topos, equalizer constructions of exponentials in a coalgebra topos and the subobject classifier of a coalgebra topos make that coalgebra category an elementary topos.

The category ${\mathcal{E}}^G$ consists of coalgebras for a comonad and their structure-preserving morphisms. Its forgetful functor has the cofree coalgebra as right adjoint. If $\mathcal{E}$ is a topos and $G$ preserves finite limits, those limits are created by the forgetful functor, while exponentials in a coalgebra topos and the subobject classifier of a coalgebra topos can be constructed as equalizers inside cofree objects.

A coherent category has finite limits, pullback-stable regular-epi/mono image factorizations, and finite unions of subobjects stable under pullback. Each subobject lattice is distributive. These structures interpret all constructors of coherent logic.

A functor between coherent categories is coherent when it preserves finite limits, image factorizations and finite unions of subobjects, including the empty union. It consequently preserves the interpretation of every coherent formula. A coherent functor from a coherent syntactic category to a topos is equivalent to a model of the corresponding coherent theory; natural transformations correspond to ordinary model homomorphisms.

A geometric morphism is essential when its inverse image has an additional left adjoint. For a functor of small categories, precomposition on presheaves has left Kan extension and Right Kan extension as its two adjoints. Precomposition preserves finite limits pointwise, so this is an essential geometric morphism.

In the Category of sets, filtered colimits commute with finite limits. Elements in a finite limiting diagram involve only finitely many representatives and finitely many equalities, all of which can be realized at one common stage of a filtered diagram.

If a category has pullbacks in a category, each slice category is finitely complete. The identity of the base object is terminal in the slice. Ambient pullbacks in a category inherit a unique common structure map to the base and satisfy the same universal property over that base. A terminal object and pullbacks in a category construct finite products in a category and equalizers, hence all finite limits.

A functor $F:\mathcal{C}\to \mathbf{Set}$ is finite-limit-preserving if it carries each finite limit cone to a limiting cone. When $\mathcal{C}$ is a small category with finite limits, this is equivalent to $F$ being a filtered colimit in a category of covariant representable functors, and to the opposite of its category of elements being a filtered category. It is also equivalent to every comma category $(S\downarrow F)$ having finite limits, for all sets $S$.

A covariant functor into a Grothendieck topos is flat when its tensor extension from presheaves preserves finite limits. For set values, its category of elements with arrows carrying source elements to target elements is cofiltered; equivalently the functor is a filtered colimit of covariant representables. If the indexing category has finite limits, flatness is equivalent to preservation of finite limits. For a site, cover-to-joint-epimorphism continuity adds the condition needed by the Diaconescu equivalence for geometric morphisms.

For a small category with finite limits, a set-valued functor preserving them has a category of elements with finite limits, so its opposite is a filtered category. The covariant density presentation is therefore a filtered colimit of representable functors. Conversely, representable functors preserve categorical limits, and filtered colimits commute with finite limits in sets, proving the criterion.

A geometric formula is built from atoms by finite conjunction, arbitrary small disjunction and existential quantification. Empty conjunction and disjunction give truth and falsity. In a Grothendieck topos, these constructions use finite limits, unions and images. Formula contexts have finitely many variables.

Objects are geometric formulas in context modulo provable equivalence. Morphisms are provably total, single-valued geometric relations; composition is existential conjunction. Conjunction and equality give finite limits. Interpreting formulas in a model gives a finite-limit-preserving functor, with the additional continuity condition supplied by the geometric syntactic topology.

The subobject classifier supplies intuitionistic truth values. Subobjects interpret predicates, finite limits interpret finite conjunctions and equality, and suitable image and adjoint constructions interpret quantifiers. One must distinguish internal intuitionistic arguments from classical reasoning in the external category of sets.

The inverse image is a finite-limit-preserving left adjoint with right adjoint $f_{\ast }$. It preserves arbitrary colimits, and hence images as well as finite limits. These properties preserve the interpretation of geometric formulas. It need not preserve Heyting implication or every universal quantifier.

A reflective subcategory is left-exact when its reflector preserves finite limits. The fixed objects of a left-exact reflector are closed under finite limits.