2025/08/08 by José Siqueira, Siqueira, José
Earth and Planetary Sciences · #03G30 #Category Theory (math.CT) #FOS: Mathematics #Geological Modeling and Analysis #Logic (math.LO)
paper · pdf · doi:10.48550/arxiv.2508.06637
openalex publication_date 2025/08/08 · openalex created_date 2025/10/10 · openalex updated_date 2026/08/01
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é 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ënius 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é). 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.