regular category = unary regular
coherent category = finitary regular
geometric category = infinitary regular
Could not include topos theory - contents
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.