A Heyting category is a coherent category in which each base change functor has a right adjoint (in addition to the left adjoint that exists in any regular category). It follows that each is a Heyting algebra and the base-change functors are Heyting algebra homomorphisms. Any Heyting category has an internal logic which is full (typed) first-order intuitionistic logic.
Any topos, and in fact any well-powered infinitary coherent category, is a Heyting category. Any Boolean category is also a Heyting category.
A Heyting functor is a coherent functor? betwen Heyting categories which additionally preserves the right adjoints . Such functors also preserve the internal interpretation of first-order logic.