On the Beck--Chevalley condition

Boolean hyperdoctrines provide an algebraic semantics for classical first-order logic with equality. In the definition of a Boolean hyperdoctrine, the Beck–Chevalley condition captures the commutativity of substitutions with quantifiers and with equality. Often, a generalization of these conditions is considered, which requires the commutativity of an appropriate square for every pullback square in the base category. A Boolean hyperdoctrine satisfying this condition is called full. Our contribution is twofold. On the negative side, we exhibit a non-full Boolean hyperdoctrine. On the positive side, we show that every Boolean hyperdoctrine $\mathsf{F}\mathsf{i}\mathsf{n}\mathsf{S}\mathsf{e}\mathsf{t}\to \mathsf{B}\mathsf{A}$ over ${\mathsf{F}\mathsf{i}\mathsf{n}\mathsf{S}\mathsf{e}\mathsf{t}}^{\mathrm{o}\mathrm{p}}$ is full.