∞-ary regular and exact categories
arity class: unary, finitary, infinitary
regularity
regular category = unary regular
coherent category = finitary regular
geometric category = infinitary regular
exactness
exact category = unary exact
A Heyting category (called a logos in Freyd-Scedrov) is a coherent category in which each base change functor has a right adjoint (the universal quantifier, in addition to the left adjoint existential quantifier that exists in any regular category).
It follows that each poset of subobjects is a Heyting algebra and the base-change functors are Heyting algebra homomorphisms. The Heyting implication can be defined as follows: if and are subobjects of , where the subobject monomorphism from to is , , where is considered as a subobject of . Any Heyting category has an internal logic which is full (typed) first-order intuitionistic logic. The extra right adjoint 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 . 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.