A characterization of regular and exact completions of pure existential completions

The notion of existential completion in the context of Lawvere’s doctrines was introduced by the second author in his PhD thesis, and it turned out to be a restriction to faithful fibrations of Peter Hofstra’s construction used to characterize Dialectica fibrations. The notions of regular and exact completions of elementary and existential doctrines were brought up in recent works by the first author with F. Pasquali and P. Rosolini, inspired by those done by M. Hyland, P. Johnstone and A. Pitts on triposes. Here, we provide a characterization of the regular and exact completions of (pure) existential completions of elementary doctrines by showing that these amount to the $𝗋𝖾𝗀/𝗅𝖾𝗑$ and $𝖾𝗑/𝗅𝖾𝗑$-completions, respectively, of the category of predicates of their generating elementary doctrines. This characterization generalizes a previous result obtained by the first author with F. Pasquali and P. Rosolini on doctrines equipped with Hilbert’s ϵ-operators. Relevant examples of applications of our characterization, quite different from those involving doctrines with Hilbert’s ϵ-operators, include the regular syntactic category of the regular fragments of first-order logic (and his effectivization) as well as the construction of Joyal’s Arithmetic Universes.