Double-functorial representation of regular hyperdoctrines

Abstract

It is well-known that pseudofunctors from bicategories of spans are equivalent to Beck-Chevalley bifibrations, and therefore capture the relationships underlying the adjunctions suitable as semantics for existential quantification. This was further expanded upon by Dawson, Par\'e and Pronk in the context of double categories. By viewing hyperdoctrines from a double-categorical lens, this paper shows that we can also characterise the Frob\"enius property: (generalised) regular hyperdoctrines correspond to certain lax symmetric monoidal pseudo double functors from spans to quintets whose monoidal laxators provide companion commuter cells (in the sense of Par\'e). This facilitates the study of the compositionality of regular hyperdoctrines and hints at a new notion of regular double hyperdoctrine. As an application, we discuss how we can recover a form of graphical regular logic suitable for modelling specifications of systems (e.g., port-plugging systems) that compose operadically.