Heyting category


Regular and Exact categories

∞-ary regular and exact categories?



Category Theory

Topos Theory

topos theory



Internal Logic

Topos morphisms

Extra stuff, structure, properties

Cohomology and homotopy

In higher category theory




A Heyting category (called a logos in Freyd-Scedrov) is a coherent category in which each base change functor f *:Sub(Y)Sub(X)f^*:Sub(Y)\to Sub(X) has a right adjoint f\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 Sub(X)Sub(X) is a Heyting algebra and the base-change functors f *f^* are Heyting algebra homomorphisms. The Heyting implication can be defined as follows: if AA and BB are subobjects of XX, where the subobject monomorphism from AA to XX is mm, (AB):= m(AB)(A\Rightarrow B) := \forall_m(A\wedge B), where ABA\wedge B is considered as a subobject of AA. Any Heyting category has an internal logic which is full (typed) first-order intuitionistic logic. The extra right adjoint f\forall_f provided by the above axiom gives the universal quantifier in this logic.

A Heyting functor is a coherent functor between Heyting categories which additionally preserves the right adjoints f\forall_f. Such functors also preserve the internal interpretation of first-order logic.


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


Last revised on April 28, 2016 at 11:53:07. See the history of this page for a list of all contributions to it.