Double-functorial representation of regular monoidal structures

TL;DR

This paper introduces a double-categorical framework to characterize regular hyperdoctrines and their Frobenius property, enabling a graphical logic for system specifications with compositional semantics.

Contribution

It extends the categorical understanding of hyperdoctrines by using double pseudofunctors to characterize regularity and Frobenius properties, proposing a new notion of regular double hyperdoctrine.

Findings

Characterizes regular hyperdoctrines via double pseudofunctors.

Shows how Frobenius property relates to monoidal laxators and companion cells.

Provides a graphical regular logic for system specifications.

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.