nLab
Heyting category

Definition

A Heyting category (called a logos in Freyd-Scedrov) is a coherent category in which each base change functor $f^{*}:\mathrm{Sub}(Y)\to \mathrm{Sub}(X)$ has a right adjoint ${\forall }_f$ (the universal quantifier, in addition to the left adjoint existential quantifier that exists in any regular category).

It follows that each poset of subobjects $\mathrm{Sub}(X)$ is a Heyting algebra and the base-change functors $f^{*}$ are Heyting algebra homomorphisms. Any Heyting category has an internal logic which is full (typed) first-order intuitionistic logic. The extra right adjoint ${\forall }_f$ provided by the above axiom gives the universal quantifier in this logic.

A Heyting functor is a coherent functor betwen Heyting categories which additionally preserves the right adjoints ${\forall }_f$. Such functors also preserve the internal interpretation of first-order logic.

Examples

Any topos, and in fact any well-powered infinitary coherent category, is a Heyting category. Any Boolean category is also a Heyting category.

References

• Peter Freyd, Andre Scedrov, Categories, Allegories