# Is every category whose subobject functor is a hyperdoctrine a Heyting category?

If $\mathsf{C}$ is a finitely complete category, we have a functor $\mathrm{Sub}: \mathsf{C}^\text{op} \to \mathsf{Pos}$, which takes an object to its poset of subobjects and a morphism to the pullback functor. If $\mathsf{C}$ is a Heyting category, then in particular its subobject functor factorizes through the forgetful functor $\mathsf{Heyt} \to \mathsf{Pos}$. Furthermore any $f: X \to Y$ in $\mathsf{C}$, the pullback functor $f^* = \mathrm{Sub}(f)$ has both a left adjoint $\exists_f$ and a right adjoint $\forall_f$ (in $\mathsf{Pos}$: these adjoints need not be Heyting algebra morphisms). These adjoints satisfy the Beck-Chevalley condition: if $$\require{AMScd} \begin{CD} A @>{f}>> B\\ @V{g}VV @V{h}VV \\ C @>{k}>> D \end{CD}$$ is a pullback square, then $$\require{AMScd} \begin{CD} \mathrm{Sub}(B) @>{f^*}>> \mathrm{Sub}(A)\\ @V{\exists_h}VV @V{\exists_g}VV \\ \mathrm{Sub}(D) @>{k^*}>> \mathrm{Sub}(C) \end{CD}$$ commutes. To summarize all this in four words: $\mathrm{Sub}$ is a hyperdoctrine.

However, a priori more is true: $\mathsf{C}$ is a coherent category, which means it has images (which are stable under pullback) and coproducts (which are stable under pullback). (Edit: my problem was that I got the definition of coherent wrong. Coherent means that the subobject lattices have pullback-stable finite joins; not the entire category. Then it is reasonably easy to prove that the conditions are sufficient.)

Do those things follow from the first set of conditions? If $\mathsf{C}$ is a finitely complete category, such that its subobject functor $\mathrm{Sub}:\mathsf{C}^\text{op} \to \mathsf{Pos}$ factorizes through the forgetful functor $\mathsf{Heyt} \to \mathsf{Pos}$, and for each $f: X \to Y$ in $\mathsf{C}$, the pullback operation $f^*$ has both adjoints which satisfy the Beck-Chevalley condition -- that is, if $\mathrm{Sub}$ is a hyperdoctrine -- is $\mathsf{C}$ a Heyting category?

• Actually, I figured out a counterexample myself: the category of sets with at most $n$ elements, for any fixed natural $n \geq 2$. – Mees de Vries Feb 6 '17 at 22:12
• Actually, on second thought, that category isn't finitely complete. So now I'm once again unsure. – Mees de Vries Feb 6 '17 at 23:29