Reference. Convolution Products on Double Categories and Categorification of Rule Algebras

Nicolas Behr, Paul-André Melliès, Noam Zeilberger · FSCD · 2023 · category-theory · DOI
Motivated by compositional categorical rewriting theory, we introduce a convolution product over presheaves of double categories which generalizes the usual Day tensor product of presheaves of monoidal categories. One interesting aspect of the construction is that this convolution product is in general only oplax associative. For that reason, we identify several classes of double categories for which the convolution product is not just oplax associative, but fully associative. This includes in particular framed bicategories on the one hand, and double categories of compositional rewriting theories on the other. For the latter, we establish a formula which justifies the view that the convolution product categorifies the rule algebra product.

Cite
Cite as @behr-2023-convolution (helia, typst) · \cite{behr-2023-convolution} (LaTeX)
BibTeX
bibtex · 14 lines
@inproceedings{behr-2023-convolution,
  doi = {10.4230/LIPICS.FSCD.2023.17},
  url = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.17},
  author = {Behr, Nicolas and Melliès, Paul-André and Zeilberger, Noam},
  keywords = {Categorical rewriting, double pushout, sesqui-pushout, double categories, convolution product, presheaf categories, framed bicategories, opfibrations, rule algebra, Theory of computation → Categorical semantics},
  language = {en},
  title = {Convolution Products on Double Categories and Categorification of Rule Algebras},
  volume = {260},
  pages = {17:1-17:20},
  publisher = {Schloss Dagstuhl – Leibniz-Zentrum für Informatik},
  year = {2023},
  copyright = {Creative Commons Attribution 4.0 International license},
  booktitle = {8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)}
}
hayagriva YAML (typst)
yaml · 17 lines
behr-2023-convolution:
  type: article
  title: Convolution Products on Double Categories and Categorification of Rule Algebras
  author:
  - Behr, Nicolas
  - Melliès, Paul-André
  - Zeilberger, Noam
  date: 2023
  page-range: 17:1-17:20
  url: https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.17
  serial-number:
    doi: 10.4230/LIPICS.FSCD.2023.17
  parent:
    type: proceedings
    title: 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)
    publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
    volume: 260
Download: behr-2023-convolution.bib · behr-2023-convolution.yml
Cited by (1)

Insights from Univalent Foundations: A Case Study Using Double Categories rasekh-2025-insightsCSL · 2025
Category theory unifies mathematical concepts, aiding comparisons across structures by incorporating not just objects, but also morphisms capturing interactions between objects. Of particular importance in some applications are double categories, which are categories with two classes of morphisms, axiomatizing two different kinds of interactions between objects. These have found applications in many areas of mathematics and theoretical computer science, for instance, the study of lenses, open systems, and rewriting. However, double categories come with a wide variety of equivalences, which makes it challenging to transport structure along equivalences. To deal with this challenge, we propose the univalence maxim: each notion of equivalence of categorical structures has a corresponding notion of univalent categorical structure which induces that notion of equivalence. We also prove corresponding univalence principles, which allow us to transport structure and properties along equivalences. In this way, the usually informal practice of reasoning modulo equivalence becomes grounded in an entirely formal logical principle. We apply this perspective to various double categorical structures, such as (pseudo) double categories and double bicategories. Concretely, we characterize and formalize their definitions in Coq UniMath up to chosen equivalences, which we achieve by establishing their univalence principles.
DOI
Cites 18 works (1 here)
With notes (1)

Framed bicategories and monoidal fibrations shulman_2008TAC · 2008

In some bicategories, the 1-cells are ‘morphisms’ between the 0-cells, such as functors between categories, but in others they are ‘objects’ over the 0-cells, such as bimodules, spans, distributors, or parametrized spectra. Many bicategorical notions do not work well in these cases, because the ‘morphisms between 0-cells’, such as ring homomorphisms, are missing. We can include them by using a pseudo double category, but usually these morphisms also induce base change functors acting on the 1-cells. We avoid complicated coherence problems by describing base change ‘nonalgebraically’, using categorical fibrations. The resulting ‘framed bicategories’ assemble into 2-categories, with attendant notions of equivalence, adjunction, and so on which are more appropriate for our examples than are the usual bicategorical ones.

We then describe two ways to construct framed bicategories. One is an analogue of rings and bimodules which starts from one framed bicategory and builds another. The other starts from a ‘monoidal fibration’, meaning a parametrized family of monoidal categories, and produces an analogue of the framed bicategory of spans. Combining the two, we obtain a construction which includes both enriched and internal categories as special cases.

Web
External (17)
behr-2023-convolution reference entries/refs/behr-2023-convolution/behr-2023-convolution.hel