Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Para construction for double categories

Bojana Femić

TL;DR

The paper develops a double-categorical Para/coPara framework by endowing a double category ${f D}$ with a horizontal action of a horizontally monoidal double category ${f M}$, producing Para$_{f M}({f D})$ and coPara$_{f M}({f D})$. Its central contribution is a robust equivalence (Theorem 1) linking lax monoidality of the action, bistrong commutativity, purely central horizontally premonoidal structure of coPara, and the extension of monoidal structure to coPara; the equivalence generalizes prior bicategorical and vertical double-categorical results to the horizontal setting and the co- (Kleisli) context. The work systematically develops the machinery for lifting vertical to horizontal structures, action theory, and locally cubical bicategories to manage coherence data, culminating in a comprehensive Para/coPara theory for double categories with broad computational and theoretical relevance. By relating extension of canonical actions, horizontality of monoidal structures, and centrality phenomena, the paper provides a unifying lens for parametric morphisms in double categories and their monoidal/comonadic interpretations. The results have potential applications in areas where double-ccategory semantics model parametric effects, such as in advanced type systems, open games, and cybernetic frameworks that leverage parametric morphisms and Kleisli-like constructions.

Abstract

We introduce Para and coPara double categories for double categories. They rely on a horizontal action $\crta\ot$ of a horizontally monoidal double category $\Mm$ on a double category $\Dd$. We prove a series of properties, most importantly, we characterize monoidality of $\coPara_\Mm(\Dd)$ in the way that it extends monoidality of $\Dd$ as: lax monoidality of the action $\crta\ot$; bistrong commutativity of $\crta\ot$; and purely central premonoidality of $\coPara_\Mm(\Dd)$.

Para construction for double categories

TL;DR

The paper develops a double-categorical Para/coPara framework by endowing a double category with a horizontal action of a horizontally monoidal double category , producing Para and coPara. Its central contribution is a robust equivalence (Theorem 1) linking lax monoidality of the action, bistrong commutativity, purely central horizontally premonoidal structure of coPara, and the extension of monoidal structure to coPara; the equivalence generalizes prior bicategorical and vertical double-categorical results to the horizontal setting and the co- (Kleisli) context. The work systematically develops the machinery for lifting vertical to horizontal structures, action theory, and locally cubical bicategories to manage coherence data, culminating in a comprehensive Para/coPara theory for double categories with broad computational and theoretical relevance. By relating extension of canonical actions, horizontality of monoidal structures, and centrality phenomena, the paper provides a unifying lens for parametric morphisms in double categories and their monoidal/comonadic interpretations. The results have potential applications in areas where double-ccategory semantics model parametric effects, such as in advanced type systems, open games, and cybernetic frameworks that leverage parametric morphisms and Kleisli-like constructions.

Abstract

We introduce Para and coPara double categories for double categories. They rely on a horizontal action of a horizontally monoidal double category on a double category . We prove a series of properties, most importantly, we characterize monoidality of in the way that it extends monoidality of as: lax monoidality of the action ; bistrong commutativity of ; and purely central premonoidality of .

Paper Structure

This paper contains 24 sections, 27 theorems, 124 equations, 1 figure, 3 tables.

Table of Contents

  1. Introduction
  2. Lifting of vertical to horizontal structures
  3. Basics on double categories and notation
  4. Companions, liftings and modifications
  5. Horizontally premonoidal double categories
  6. Binoidal double categories and central cells
  7. Horizontally premonoidal double categories
  8. Locally cubical bicategories of (monoidal) double categories
  9. Double categories of (monoidal) double functors
  10. Double category of vertically monoidal double functors
  11. Double category of horizontally monoidal double functors
  12. Lifting of vertical to horizontal monoidal double structures
  13. The announced locally cubical bicategories
  14. Actions on double categories
  15. Monoidal actions of double categories
  16. ...and 9 more sections

Key Result

Corollary 2.3

Let $u$ be an invertible 1v-cell. If $u^{-1}$ has a companion $\widehat{(u^{-1})}$, then $u$ has a conjoint given by $\check u=\widehat{(u^{-1})}$ with $\varepsilon^*_u=\frac{\varepsilon_{u^{-1}}}{\operatorname {Id}^u}$ and $\eta^*_u=\frac{\operatorname {Id}^u}{\eta_{u^{-1}}}$.

Figures (1)

  • Figure :

Theorems & Definitions (70)

  • Definition 2.1
  • Definition 2.2
  • Corollary 2.3
  • Proposition 2.4
  • Definition 2.5
  • Definition 2.6
  • Proposition 2.7
  • Proposition 2.8
  • Definition 3.1
  • Definition 3.2
  • ...and 60 more