📝 SummarXiv

Abstract

It is well-known that pseudo functors 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 Frobenius property: (generalised) regular hyperdoctrines correspond to those lax symmetric monoidal double pseudofunctors from spans to quintets whose monoidal laxators provide companion commuter cells (in the sense of Par\'e). This suggests 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.