∞-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). Thus, every Heyting category is a first-order hyperdoctrine given by the subobject poset functor .
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 , then we can define as , where is the subobject inclusion and we take . 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. On the other hand, any category defined in intuitionistic logic which satisfies bounded separation is a Heyting category.
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.
Every locally cartesian closed coherent category is a Heyting category, because the dependent product functors preserve monomorphisms. This implies that every Pi-pretopos is a Heyting pretopos.
In particular, the h-sets in Martin-Löf type theory with propositional truncations form a Heyting category.
Last revised on September 13, 2024 at 22:43:36. See the history of this page for a list of all contributions to it.