Double-functorial representation of regular monoidal structures
Fuente:
arXiv
Enregistré dans:
| Auteur principal: | |
|---|---|
| Format: | Preprint |
| Publié: |
2025
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866908556938182656 |
|---|---|
| author | Siqueira, José |
| author_facet | Siqueira, José |
| contents | 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é 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é). 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2508_06637 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Double-functorial representation of regular monoidal structures Siqueira, José Category Theory Logic 03G30 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é 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é). 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. |
| title | Double-functorial representation of regular monoidal structures |
| topic | Category Theory Logic 03G30 |
| url | https://arxiv.org/abs/2508.06637 |