Is there an intuitively-reasonable hyperdoctrine for classical first-order logic that doesn't satisfy the Frobenius condition, eg where $[\exists y. P^*(x) \land Q(x, y)] \ne [P(x) \land \exists y. Q(x, y)]$, where $P^*$ denotes the weakening of the 1-arity predicate $P$ to a 2-arity predicate?
For instance & in case the question is unclear as stated, in this discussion, Michael Weiss and John Baez discuss how a hyperdoctrine allegedly needs to satisfy the Frobenius condition to model the traditional axioms of first-order logic.
To be clear, I'm looking answers in the rough class "if you interpret formulas as talking about these particular Boolean algebras in this particular way, you'll find that it's quite intuitively reasonable for the theory to deny $P(x) \implies \exists y. P^*(x)$". Obviously, the syntactic model of first-order logic less the law that existential quantification distributes over conjunction is a hyperdoctrine that technically provides a counterexample, but this is pretty unsatisfying.
And, fwiw, I wouldn't mind a bunch of examples from intuitionistic first-order logic if it's particularly tricky to find a non-pathological classical example for one reason or another :-)