Quantifier alternation depth in universal Boolean doctrines

We introduce the notion of a quantifier-stratified universal Boolean doctrine. This notion requires additional structure on a universal Boolean doctrine, accounting for the quantifier alternation depth of formulas. After proving that every Boolean doctrine over a small base category admits a quantifier completion, we show how to freely add the first layer of quantifier alternation depth to these doctrines. To achieve this, we characterize, within the doctrinal setting, the classes of quantifier-free formulas whose universal closure is valid in some common model.