A 2-category is Heyting if it is coherent and each pullback functor has a right adjoint .
As in the 1-categorical case, this also ensures that each is a Heyting algebra and that each is a homomorphism of Heyting algebras. Moreover, the right adjoints satisfy the Beck-Chevalley condition for pullback squares, because the left adjoints do. This is just what is necessary for the internal interpretation of (finitary) first-order logic.
A 1-category is Heyting as a 2-category iff it is Heyting as a 1-category.
A (0,1)-category is Heyting iff it is a Heyting algebra.
Any well-powered infinitary-coherent 2-category is Heyting, by the adjoint functor theorem for posets. In particular, any Grothendieck 2-topos is Heyting.
Unlike in the 1-categorical case, there seems no reason why a coherent 2-category with exponentials must be Heyting. It does, however have adjoints to pullback along fibrations and opfibrations, and in particular along product projections, which is enough for some uses of universal quantification in the internal logic.
Clearly if is Heyting, so are , , , , and (the Heyting algebra of subterminals).
Moreover, Heytingness is also preserved by fibrational slicing. First we show:
If is Heyting, then for any and any , is a coreflective sub-poset of .
As proven here, is a full sub-poset of . Moreover, it is easy to see that a ff is in precisely when
In general, the first condition does not imply the second. It is also easy to check that these two conditions together are equivalent to saying that the composite
factors through , where is the action making into a fibration. Note that is alternately written as , where is the projection onto the first factor. Therefore, is in just when , or equivalently when .
We claim that coreflects into , and given the above, it suffices to verify that it is a comonad. First, let be the inclusion of identities; then and , so we have
This gives the counit of the comonad. The comultiplication is a little more involved. First note that we have a pullback square
where denotes projection onto the first two factors. Thus, by the Beck-Chevalley condition, and therefore
where is the “composition” morphism.
Let us write for , the object of composable arrows in , and write for the power of with the category
Let forget the “lonely” arrow, and let make the lonely arrow into the composite of the other two. Then , and moreover , where and are and applied to the non-lonely arrows. Thus, we have
as desired. (Here we have used another Beck-Chevalley condition to move past and , turning them into and and it into .)
If is Heyting, so is each fibrational slice and .
This follows from the adjoint lifting theorem for posets: for any in we have a commutative square
where the vertical arrows are comonadic (inclusions of coreflective sub-posets) and the bottom horizontal arrow has a right adjoint; hence so does the top horizontal arrow.
We may naturally say that a coherent 2-category is Boolean if each is a Boolean algebra. As usual, this implies that is Heyting; we have .
Note that a subobject and its complement in need not be “disjoint” in the sense introduced here; only their pullback, not their comma object, need be initial. Note also that unlike in the 1-categorical case, Booleanness is not stable under slicing; this fails already in the (1,2)-category (though it holds in any (2,1)-category).