# Convolution Products on Double Categories and Categorification of Rule Algebras

Nicolas Behr, Paul-André Melliès, Noam Zeilberger

► To cite this version:

Nicolas Behr, Paul-André Melliès, Noam Zeilberger. Convolution Products on Double Categories and Categorification of Rule Algebras. FSCD 2023 - 8th International Conference on Formal Structures for Computation and Deduction, Jul 2023, Rome, Italy. pp.17:1-17:20, 10.4230/LIPIcs.FSCD.2023.17 . hal-04222049

HAL Id: hal-04222049

https://hal.science/hal-04222049v1

Submitted on 24 Nov 2023

**HAL** is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons CC BY 4.0 - Attribution - International License
# Convolution Products on Double Categories and Categorification of Rule Algebras

Nicolas Behr ⬒ ID

CNRS, Université Paris Cité, IRIF, France

Paul-André Melliès ⬒ ID

CNRS, Université Paris Cité, INRIA, France

Noam Zeilberger ⬒ ⬅

École Polytechnique, LIX, Palaiseau, France

## Abstract

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.

**2012 ACM Subject Classification** Theory of computation → Categorical semantics

**Keywords and phrases** Categorical rewriting, double pushout, sesqui-pushout, double categories, convolution product, presheaf categories, framed bicategories, opfibrations, rule algebra

Digital Object Identifier 10.4230/LIPIcs.FSCD.2023.17

## 1 Introduction

Our main motivation in this work is to categorify notions coming from compositional rewriting theory in the sense of [1–5, 8, 9] and more specifically the concepts of rule algebra [1, 3, 8, 9] and of tracelet [2, 6]. There, a rewriting theory is specified by a base category $C$ together with a specific categorical description of direct derivations, defined as rewriting steps $s: X \to Y$ obtained by applying a rewriting rule $r: A \to B$ to a given object $X \in C$ of the base category. Typical descriptions include double-pushout (DPO) [13] and sesqui-pushout (SqPO) [10] formalisms. A rewriting theory defined in this way is called compositional when it satisfies a technical property of two- and three-step derivation traces, ensuring that the two theorems below are satisfied:

- the concurrency theorem [1, 4, 5, 7, 13] states that every two-step derivation trace may be (essentially uniquely) characterized by a one-step trace (i.e., a direct derivation) along a composite rule capturing the causal interactions between the two rules,

- the associativity theorem [1, 4, 5, 7, 9] states that whenever the concurrency theorem is applied twice in order to convert a three-step trace into a one-step trace along a composite rule, either possible nesting order of two-step rule composition operations yields essentially the same one-step trace (i.e., up to universal isomorphisms).

One important benefit of compositionality is that every compositional rewriting theory gives rise to a rule algebra defined as a vector space $\mathcal{R}$ (over a suitable field $k$ such as $k = \mathbb{R}$) with a basis indexed by (isomorphism classes of) rules, and equipped with a bilinear product that maps a pair of basis elements to a sum over basis elements indexed by composite rules. More

<figure><img src="image_2.png" /></figure>

© Nicolas Behr, Paul-André Melliès, and Noam Zeilberger; licensed under Creative Commons License CC-BY 4.0

8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023).

Editors: Marco Gaboardi and Femke van Raamsdonk; Article No. 17; pp. 17:1–17:20

<figure><img src="image_3.png" /></figure>

LIPICS

Leibniz International Proceedings in Informatics

Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany
17:2 Convolution Products on Double Categories and Categorification of Rule Algebras

explicitly, letting $\delta(r)$ denote the basis vector of $\mathcal{R}$ indexed by (the isomorphism class of) a
rule $r$, writing $\star$ for the aforementioned binary product, $M_r(s)$ for admissible matches of
rule $r$ into rule $s$, we have

$$
\delta(r) \star \delta(s) = \sum_{\mu \in \mathcal{M}_r(s)} \delta(r_\mu s) \qquad (1)
$$

where $r_\mu s$ denotes one possible way to obtain a composite rule from $r$ and $s$. Another
natural idea when reasoning about compositional rewriting systems is to study sets of direct
derivations as follows: we introduce a vector space $\mathcal{S}$ together with a notation $|X\rangle$ for a basis
vector of $\mathcal{S}$ indexed by an (isomorphism class of an) object $X$ of the underlying category.
We then define the algebra morphism (or representation) $\rho: \mathcal{R} \to \mathrm{End}_{\mathcal{K}}(\mathcal{S})$ as follows:

$$
\rho(\delta(r)) |X\rangle := \sum_{m \in M_r(X)} |r_m(X)\rangle, \qquad (2)
$$

where the right-hand side of the equation ranges over possible matches $m \in M_r(X)$ of the
rule $r$ into the object $X$, and where $|r_m(X)\rangle$ is the vector indexed by the isomorphism class
of the outcome of applying $r$ to $X$ via $m$. The crucial fact that $\rho$ satisfies the equation

$$
\rho(\delta(r))\rho(\delta(s)) = \rho(\delta(r) \star \delta(s)) \qquad (3)
$$

and thus defines a *representation in S of the rule algebra (R,★)* is far from trivial, and comes
from a subtle interplay between the concurrency and the associativity theorems [1, 4, 5, 7, 9].

In the present paper, our primary purpose is to begin to categorify the rule algebra
formalism, starting from the observation that the traditional frameworks for categorical
rewriting (including the double-pushout and sesqui-pushout formalisms) can be neatly
expressed using double categories. The idea is to associate to any such categorical rewriting
framework a specific double category $\mathbb{D}$ whose objects are the objects of the original base
category $\mathbf{C}$ and whose horizontal 1-cells $X \to Y$ are transformations typically defined as
spans $X \leftarrow S \to Y$ in $\mathbf{C}$, defined in such a way that they include both the rewriting rules
$r: A \to B$ as well as the derivation traces $s: X \to Y$ of the underlying rewriting theory.
The double category $\mathbb{D}$ is then carefully designed in such a way that a direct derivation $\theta$
applying the rewriting rule $r: A \to B$ to define a rewriting step $s: X \to Y$ is the same thing
as a double cell $\theta: r \to s$ of the form below, in the double category $\mathbb{D}$.

$$
\begin{tikzcd}[column sep=2.8em, row sep=2.8em]
    B \arrow[r, "r"] \arrow[d, "g"] & A \arrow[d, "\theta"] \\
    Y \arrow[r, "s"] & X
\end{tikzcd}
\qquad (4)
$$

Here, the vertical maps $f$ and $g$ of the double category $\mathbb{D}$ indicate how the source $A$ and the target $B$ of the rewriting rule $r: A \to B$ are “embedded” in the objects $X$ and $Y$, respectively, in order to define the direct derivation $\theta: r \to s$ exhibiting $s: X \to Y$ as an instance of the rewriting rule $r$. Given a rewriting rule $r: A \to B$ and a horizontal 1-cell $s: X \to Y$, it makes sense to look at the set $\hat{\Delta}_r(s)$ of double cells $\theta: r \to s$ of the form (4), which describes all the possible embeddings $f: A \to X$ and $g: Y \to B$ and all the possible ways $\theta: r \to s$ the horizontal 1-cell $s: X \to Y$ can be seen as an instance of the rewriting rule $r$. An important observation is that $\hat{\Delta}_r$ defines a covariant presheaf $\hat{\Delta}_r: \mathbb{D}_1 \to \mathbf{Set}$ over the vertical cell category $\mathbb{D}_1$ whose objects are horizontal 1-cells, and whose morphisms $\varphi: s \to s'$ are double cells of the form

$$
\begin{tikzcd}[column sep=2.8em, row sep=2.8em]
    Y \arrow[r, "s"] \arrow[d, "h_Y"] & X \arrow[d, "h_X"] \\
    Y' \arrow[r, "s'"] & X''
\end{tikzcd}
\qquad (5)
$$
where the category $\mathbb{D}_1$ appears $n$ times and $\mathbb{D}_0$ appears $n+1$ times. The objects (respectively morphisms) of $\mathbb{D}_n$ may be seen as sequences $(s_n, \dots, s_1)$ of $n$ composable horizontal 1-cells (resp. double cells), with the functor

$$h_n = (s_n, \dots, s_1) \mapsto h_n(s_n, \dots, s_1) \in \mathrm{obj}(\mathbb{D}_1)$$

performing the horizontal composition “all at once”. In this *presentation*, both associativity and neutrality are represented by a single family of natural isomorphisms

$$h_n \circ (h_{i_1}, \dots, h_{i_n}) \cong h_{i_1+\dots+i_n}$$

satisfying a number of coherence axioms.

We will go back and forth between the biased and unbiased definitions of a double category, which are equivalent. In particular, given a double category with unit $U$ and (binary) horizontal composition $\diamond_h$, we can obtain a family of $n$-ary composition functors $h_n$ by taking $h_0 = U$, $h_1 = id$, and $h_n$ to be any bracketing of $n-1 \diamond_h$'s for $n \ge 2$.

# 3 A convolution product of presheaves over double categories

## 3.1 Presheaves over double categories and the convolution product

One starting point for our work was the observation that the Day convolution product on presheaves over monoidal categories [11] may be extended to a convolution product for *vertical presheaves* over double categories. As explained in the introduction, a *vertical presheaf* over a double category $\mathbb{D}$ is simply defined as a covariant *Set*-valued presheaf over the category $\mathbb{D}_1$ whose objects are the horizontal 1-cells and whose morphisms are the double cells of $\mathbb{D}$. We write $\hat{\mathbb{D}} = [\mathbb{D}_1, \mathrm{Set}]$ for the category of vertical presheaves over $\mathbb{D}$ and natural transformations between them. A vertical presheaf $F$ over a double category $\mathbb{D}$ thus assigns a set $F(r)$ to every horizontal 1-cell $r: Y \leftarrow X$, and a function $F(\alpha): F(r) \to F(r')$ to every double cell $\alpha: r \to r'$. As also explained in the introduction, an important example is provided by *representable presheaves*, which we notate $\hat{\Delta}_r := \mathbb{D}_1(r, -)$.

**► Example 3.1.** Term rewriting systems may be modeled as vertical presheaves over the double category TRS[$\Sigma$]. For example, suppose $\Sigma$ contains a binary operation $m$ and a constant $e$, and consider the rewriting rule $r: m(e, x) \to x$. The presheaf $\hat{\Delta}_r$ in a sense encapsulates all ways of applying $r$ once to a subterm. For instance, $\hat{\Delta}_r(r': m(e, m(e, x)) \to m(e, x))$ contains exactly two elements, corresponding to the double cells $\alpha_1: r \to r'$ and $\alpha_2: r \to r'$ defined by the context/substitution pairs $(C_1 = - | \sigma_1 = m(e, x)/x)$ and $(C_2 = m(e, -) | \sigma_2 = x/x)$ respectively.

At this stage, we explain how we extend the Day convolution product to double categories. We find it instructive to begin by recalling the usual definition of the Day convolution product on presheaves over a category $\mathcal{C}$ equipped with a monoidal product $\otimes: \mathcal{C} \times \mathcal{C} \to \mathcal{C}$. Given a pair of presheaves $G$ and $F$ over $\mathcal{C}$, the convolution product $G * F$ is defined as the left Kan extension of the presheaf over the product category $\mathcal{C} \times \mathcal{C}$

$$C \times C \xrightarrow{G \times F} \mathrm{Set} \times \mathrm{Set} \xrightarrow{\times} \mathrm{Set}$$

along the monoidal product functor $\otimes$:

<figure><img src="image_4.png" /></figure>
<figure><img src="image_5.png" /><figcaption>Figure 1 Left: diagram illustrating an element of the convolution product $F_2 * F_1$ evaluated at a horizontal cell $r$, where $\alpha_1 \in F_1(s_1)$ and $\alpha_2 \in F_2(s_2)$, and $\gamma : s_2 \diamond_h s_1 \to r$. Right: equivalence relation on diagrams induced by the coend formula.</figcaption></figure>

## 3.2 Oplax associativity of the convolution product

The binary convolution product naturally generalizes to an n-ary convolution product of presheaves, defined in terms of the functors $h_n : \mathbb{D}_n \to \mathbb{D}_1$ discussed in Section 2.

**Definition 3.4.** Let $F_1, \dots, F_n : \mathbb{D}_1 \to \text{Set}$ be an n-tuple of covariant presheaves over $\mathbb{D}_1$. We define their convolution product by the coend formula

$$F_n * \dots * F_1 = r \mapsto \int^{(s_n, \dots, s_1) \in \mathbb{D}_n} \mathbb{D}_1(h_n(s_n, \dots, s_1), r) \times F_n(s_n) \times \dots \times F_1(s_n) \quad (10)$$

with the understanding that the formula specializes to $r \mapsto \int^{X \in \mathbb{D}_0} \mathbb{D}_1(U_X, r)$ in the nullary case $n = 0$. Equivalently, $F_n * \dots * F_1$ is defined by the following left Kan extension diagram:

$$\begin{tikzcd}
    \mathbb{D}_n \arrow[r, "\text{proj}"] \arrow[d, "h_n"] & \mathbb{D}_1^n \arrow[r, "F_n \times \dots \times F_1"] \arrow[d] & \text{Set}^n \arrow[r, "\times"] \arrow[d, "F_n * \dots * F_1"] & \text{Set} \\
    \mathbb{D}_1 & & &
\end{tikzcd} \quad (11)$$

For convenience, we write $*_n : \hat{\mathbb{D}}^n \to \hat{\mathbb{D}}$ for the resulting n-ary convolution product, and we also sometimes write $\bar{U}$ for the nullary case $\bar{U} = *_0$.

We find it evocative to visualize the elements of the convolution product $F_n * \dots * F_1$ evaluated at a horizontal 1-cell $r$ by a kind of “rabbit diagram”, as illustrated on the left side of Figure 1 for the case $n = 2$. In the diagram, $\alpha_1$ and $\alpha_2$ represent elements of $F_1(s_1)$ and $F_2(s_2)$ respectively, where $s_1$ and $s_2$ are arbitrary horizontal 1-cells, and $\gamma$ represents a double cell $s_2 \diamond_h s_1 \to r$ with $S(\gamma) = f$ and $T(\gamma) = g$. (We will sometimes omit the labels of the various cells in diagrams when they are unimportant.) On the right side of the figure, we also depict the equivalence relation on tuples

$$(\gamma \diamond_v (\beta_1 \diamond_h \beta_2), \alpha_2, \alpha_1) \sim (\gamma, F_2(\beta_2)(\alpha_1), F_1(\beta_1)(\alpha_1)) \quad (12)$$

that is forced by the coend formula (8).

Perhaps surprisingly, it turns out that in general convolution only defines an *oplax* monoidal product on the presheaf category $\hat{\mathbb{D}}$.
17:8 Convolution Products on Double Categories and Categorification of Rule Algebras

**▶ Theorem 3.5.** The convolution product on the category $\hat{\mathbb{D}}$ of vertical presheaves is oplax associative and oplax unital in the sense that there exists a family of natural transformations

<figure><img src="image_6.png" /></figure>

satisfying the coherence laws of an oplax monoidal product. In other words, $\hat{\mathbb{D}}$ is an oplax monoidal category under the convolution product functors $*_{n} : \hat{\mathbb{D}}^{n} \to \hat{\mathbb{D}}$.

An illustrative example is given by the natural transformations

$$ (F_3 * F_2) * F_1 \leftarrow \xrightarrow{p_{2,1}} F_3 * F_2 * F_1 \xrightarrow{p_{1,2}} F_3 * (F_2 * F_1) $$

for any triple $(F_3, F_2, F_1)$ of presheaves of $\hat{\mathbb{D}}$. To understand these natural transformations, let us consider the following diagrams, which depict generic elements of $(F_3 * F_2) * F_1$, $F_3 * F_2 * F_1$, and $F_3 * (F_2 * F_1)$ evaluated at a horizontal 1-cell $r$:

<figure><img src="image_7.png" /></figure>

Here $s_1, s_2, s_3, t$ are horizontal 1-cells, $\beta, \gamma$, and $\delta$ are double cells, and each $\alpha_i$ is an element of $F_i(s_i)$, while $f, \dots, k$ are vertical 1-cells corresponding to the projections of the respective double cells $f = T(\delta), g = T(\gamma), h = S(\gamma), i = S(\delta), j = T(\beta), k = S(\beta)$. The diagram in the middle of (13) may be seen as a degenerate case of the ones on the outside, in the sense that it corresponds to taking $\gamma$ to be the identity double cell (on $s_3 \diamond_h s_2$ and $s_2 \diamond_h s_1$ respectively) and taking $\delta = \beta$. This simple observation yields the natural transformations $p_{2,1}$ and $p_{1,2}$. On the other hand, these natural transformations need not be invertible in general for an arbitrary double category, since the diagrams on the outside of (13) cannot necessarily be transformed into the one in the middle, in particular if the vertical 1-cells $g$ and $h$ are non-trivial.

One special case where the oplaxity maps are easily seen to be invertible is when the underlying vertical category $\mathcal{D}_0$ is discrete, i.e., when $\mathcal{D}$ is a bicategory.

**▶ Definition 3.6.** We say the convolution product on $\hat{\mathbb{D}}$ is strongly associative if the natural transformations $p_{n_1, \dots, n_k}$ of Theorem 3.5 are invertible for all $n_1, \dots, n_k \ge 1$. We say that it is strongly associative and unital if the $p_{n_1, \dots, n_k}$ are invertible for all $n_1, \dots, n_k \ge 0$.

**▶ Proposition 3.7.** If $\mathcal{D}_0$ is a discrete category then the convolution product on $\hat{\mathbb{D}}$ is strongly associative and unital.

Proposition 3.7 covers in particular the case of the usual Day convolution product on presheaves over a monoidal category, seen as a double category over the terminal category $\mathcal{D}_0 = 1$. In Section 5 we will establish sufficient conditions under which the convolution product is strongly associative and unital. First, though, let us take a bit of time to consider a well-known class of double categories for which it turns out that the convolution product is strongly associative, but not strongly unital.
17:10 Convolution Products on Double Categories and Categorification of Rule Algebras

Note that here we rely on the covariant action of the presheaves $F_3$ and $F_2$ to extend the elements $\alpha_3 \in F(s_3)$ and $\alpha_2 \in F(s_2)$ by the respective op-Cartesian triangles to obtain elements of $F_3(\langle g \rangle s_3)$ and $F_2(s_2 \langle h \rangle)$. It is routine to verify that the transformation (15) defines an inverse to the natural transformation $p_{2,1} : F_3 * F_2 * F_1 \to (F_2 * F_2) * F_1$: the equation $q_{2,1} \circ p_{2,1} = id$ is trivial, while the equation $p_{2,1} \circ q_{2,1} = id$ holds because the two sides of (15) are equivalent modulo equation (12) (cf. right side of Figure 1). This argument generalizes easily to inverting $p_{n_1, \dots, n_k}$ for any $n_1, \dots, n_k \ge 1$. ◀

However, the proof of the invertibility of the natural transformations $p_{n_1, \dots, n_k}$ does not extend to arbitrary sequences of non-negative integers $n_1, \dots, n_k \ge 0$, and indeed in general the convolution product on presheaves over framed bicategories is not strongly unital. Before demonstrating this, we first state an easy observation about representability of the nullary convolution product in the presence of an initial object.

**Proposition 4.4.** If $\mathcal{D}_0$ has an initial object $0$, then $\bar{U} \cong \hat{\Delta}_{U_0}$.

**Example 4.5** (Counterexample to unitality of convolution over framed bicategories). Consider the framed bicategory $\mathbf{Span}$, and let us write $\mathbf{Span}_1$ for its underlying category of spans and double cells between them. Since $\mathbf{Set}$ has an initial object given by the empty set $\emptyset$, the nullary convolution is representable (Prop. 4.4) by $U\emptyset = \emptyset \leftarrow \emptyset \to \emptyset$. Note that the functor $U : \mathbf{Set} \to \mathbf{Span}$ has a right adjoint given by the functor sending a span $Y \leftarrow Z \to X$ to its underlying carrier $Z$, which implies (and indeed it is easy to verify) that $\emptyset \leftarrow \emptyset \to \emptyset$ is itself an initial object in $\mathbf{Span}$. This entails that $\bar{U}$ is isomorphic to the terminal presheaf on $\mathbf{Span}$.

Now, let $F = \hat{\Delta}_{U_1}$ be the presheaf represented by the identity span over the one-element set. By the aforementioned adjunction, for an arbitrary span $r = Y \leftarrow Z \to X$, elements of $F(r) \cong \mathbf{Span}(U_1, r)$ are in bijection with elements of $Z$, that is $F(r) \cong Z$. In particular, $F(r)$ is empty if $Z$ is empty. On the other hand, since $U_Y \diamond_h r \xrightarrow{\sim} r$ and since $\bar{U}(r) \cong \{*\}$, every element of $F(U_Y) \cong Y$ induces an element of $(F * \bar{U})(r)$. So $(F * \bar{U})(r)$ is non-empty if $Y$ is non-empty. But this implies that there is no natural transformation $q_{1,0} : F * \bar{U} \to F$, and hence the oplax unitor $p_{1,0} : F \to F * \bar{U}$ is not invertible.

**5 Associativity from the positive cylindrical decomposition property**

**5.1 Cylindrical Decomposition Property**

At this point, it must be stressed that our motivating examples of double categories coming from rewriting theory are *not* framed bicategories. For many of these examples, each of the source and target functors $S, T : \mathcal{D}_1 \to \mathcal{D}_0$ separately has some kind of opfibrational structure (or multi-opfibrational structure, see [5]), yet the pairing $(T, S) : \mathcal{D}_1 \to \mathcal{D}_0 \times \mathcal{D}_0$ is typically not an opfibration, because pushing one end of a horizontal 1-cell along a vertical 1-cell will not leave the other end fixed. Nevertheless, we will see that such double categories admit a strongly associative convolution product.

As an illustration, consider the *double category* $\mathcal{DPO} = \mathcal{DPO}(\mathbf{Set})$ defined as a sub-double category of $\mathbf{Span} = \mathbf{Span}(\mathbf{Set})$ with the same 0-cells and horizontal 1-cells, but restricting vertical 1-cells to injections, and restricting double cells to pairs of pushout squares:

$$ \begin{tikzcd} Y \arrow[r, "X"] \arrow[d, "X'"'] & Y' \arrow[r, "X"] \arrow[d, "X'"'] & \end{tikzcd} = \begin{tikzcd} Y \arrow[r, "X"] \arrow[d, "X'"'] & Y' \arrow[r, "X"] \arrow[d, "X'"'] & \end{tikzcd} $$
(DPO and similar double categories play a role in DPO-rewriting, see [5].) Now suppose that we want to push a span of the form $Y \leftarrow \emptyset \rightarrow X$ along a pair of injective functions $Y \rightarrow Y'$ and $X \rightarrow X'$:

<figure><img src="image_8.png" /></figure>

Such a horn may be completed to a double cell in DPO just in case there exists a set $Z'$ such that $Y' \cong Y + Z'$ and $X' \cong X + Z'$. But it is easy to construct examples for which no such set exists, for instance taking $|X| = |Y| = 1$, $|Y'| = 2$, and $|X'| = 3$. So the functor $(T, S) : \text{DPO} \rightarrow \text{Inj} \times \text{Inj}$ is not an opfibration.

However, despite DPO not being a framed bicategory, let us observe that it enjoys a similar factorization property to the one used in the proof of Theorem 4.3, and which is sufficient for proving associativity.

**► Definition 5.1.** We say that a double category $\mathcal{D}$ has the $n$-cylindrical decomposition property if for every globular cell $\rho : h_n(r_n, \dots, r_1) \to r$ and for every double cell $\varphi : r \to s$ there exists a family of $n$ double cells $(\varphi_n, \dots, \varphi_1) : (r_n, \dots, r_1) \to (s_n, \dots, s_1)$ in $\mathcal{D}_n$ and a globular cell $\sigma : h_n(s_n, \dots, s_1) \to s$ such that

$$ \varphi \diamond_v \rho = \sigma \diamond_v h_n(\varphi_n, \dots, \varphi_1) \quad (16) $$

which means that the double cell $\varphi \diamond_v \rho$ factors as the vertical composition $\sigma \diamond_v h_n(\varphi_n, \dots, \varphi_1)$ of the globular cell $\sigma$ after the horizontal composition $h_n(\varphi_n, \dots, \varphi_1)$, as depicted below:

<figure><img src="image_9.png" /></figure>

Moreover, the family of $n$ cells $(\varphi_n, \dots, \varphi_1)$ and the globular cell $\sigma$ are universal, in the sense that for every family of $n$ double cells $(\chi_n, \dots, \chi_1) : (r_n, \dots, r_1) \to (t_n, \dots, t_1)$ in $\mathcal{D}_n$, for every globular cell $\tau : h_n(t_n, \dots, t_1) \to t$ and for every double cell $\psi : s \to t$ such that the equation

$$ \psi \diamond_v \varphi \diamond_v \rho = \tau \diamond_v h_n(\chi_n, \dots, \chi_1) \quad (17) $$

holds, as depicted below

<figure><img src="image_10.png" /></figure>
Once again, the reason $q_{2,1}$ defines an inverse to $p_{2,1}$ boils down to the fact that the two sides of (20) are equated by the coend formula defining the convolution product (recall Figure 1). A similar argument can also be used to establish strong unitality when the underlying double category $\mathcal{D}$ also has the 0-CDP.

Note however that neither example of $\mathcal{S}$pan nor $\mathcal{D}$PO has the 0-CDP. It turns out nevertheless that convolution over the latter is strongly unital, as we will briefly address in Section 5.4.

## 5.2 Relative opfibrations

Here we explain how the cylindrical decomposition property can be reformulated in fibrational terms, for a natural common generalization of the notions of Grothendieck opfibration and of Street opfibration.

Let $F : E \to B$ be a functor, and let $G \stackrel{\iota}{\to} B$ be a wide subcategory of $B$ (i.e., $\iota$ is bijective on objects). We define a new category $F[G]$ as the category whose objects are given by triples $(e, b, \gamma)$ of an object $e \in E$, an object $b \in B$, and an arrow $\gamma : Fe \to b$ in $G$, and whose morphisms

$$ (e, b, \gamma) \xrightarrow{(\varepsilon, \beta)} (e', b', \gamma') $$

are given by pairs of morphisms $\varepsilon : e \to e'$ and $\beta : b \to b'$ such that $\beta \circ \gamma = \gamma' \circ F\varepsilon$. This category comes equipped with evident forgetful functors $\pi_E : F[G] \to E$ and $\pi_B : F[G] \to B$. Moreover, there is a functor $in_E : E \to F[G]$ defined on objects by $in_E(e) = (e, Fe, id_{Fe})$, in such a way that $F = \pi_B \circ in_E$. We remark that the functor $in_E$ is a left adjoint to the functor $\pi_E$, since

$$ \begin{align} \mathrm{Hom}_{F[G]}(in_E(e), (e', b', \gamma')) &= \mathrm{Hom}_{F[G]}((e, Fe, id_{Fe}), (e', b', \gamma')) \tag{21} \\ &= \{(\varepsilon, \beta) \mid \varepsilon : e \to e', \beta : Fe \to b', \beta \circ id_{Fe} = \gamma' \circ F\varepsilon\} \nonumber \\ &\cong \mathrm{Hom}_E(e, e') = \mathrm{Hom}_E(e, \pi_E((e', b', \gamma'))). \nonumber \end{align} $$

The construction generalizes to every wide subcategory $G \stackrel{\iota}{\to} B$ the construction of the free opfibration $\pi_B : F[G] \to B$ associated to a functor $F : E \to B$, which one recovers when $G$ is the category $B$ itself. This leads us to the following definition:

**Definition 5.6.** Let $F : E \to B$ be a functor, and let $G$ be a wide subcategory of $B$. We say that $F$ is a $G$-relative opfibration if $\pi_B : F[G] \to B$ is a Grothendieck opfibration.

**Example 5.7.** The definition above subsumes three standard notions of functor $F : E \to B$:

- When $G = |B|$ is the discrete wide subcategory of $B$, a $G$-relative opfibration is the same thing as a Grothendieck opfibration $F : E \to B$,

- When $G = \mathrm{core}(B)$ is the wide subcategory of reversible maps in $B$, a $G$-relative opfibration is the same thing as a Street opfibration $F : E \to B$,

- When $G = B$ is the category $B$ itself, a $G$-relative opfibration $F : E \to B$ is the same thing a general functor $F : E \to B$.

Moreover, one can readily verify that the cylindrical decomposition property we introduced above (Def. 5.1) corresponds to the following particular instance of $G$-relative opfibration.

**Proposition 5.8.** A double category $\mathcal{D}$ satisfies the n-CDP precisely when the functor $h_n : \mathcal{D}_n \to \mathcal{D}_1$ is a globular opfibration, that is, a $G$-relative opfibration where $G = \mathcal{D}_1^\bullet$ is the wide subcategory of $\mathcal{D}_1$ of globular double cells.
17:14 Convolution Products on Double Categories and Categorification of Rule Algebras

The reason is that the category $h_n[G]$ can be neatly described as the category of *cylindric maps* whose objects the tuples $(s_1, \dots, s_n, s, \sigma)$ where $\sigma : h_n(s_n, \dots, s_1) \to s$ is a globular double cell, and whose morphisms

$$ (\psi_n, \dots, \psi_1, \psi) : (s_n, \dots, s_1, s, \sigma) \to (t_n, \dots, t_1, t, \tau) $$

consist of a family of $n$ double cells $(\psi_n, \dots, \psi_1) : (s_n, \dots, s_1) \to (t_n, \dots, t_1)$ in $\mathbb{D}_n$ and of a double cell $\psi : s \to t$ in $\mathbb{D}_1$ satisfying the equation

$$ \psi \diamond_v \sigma = \tau \diamond_v h_n(\psi_n, \dots, \psi_1). $$

depicted in (19).

5.3 Kan extensions along relative opfibrations

We now state a basic result on left Kan extensions along G-relative opfibrations, analogous to a standard result about Kan extension along Grothendieck opfibrations that is extremely useful in practice:

**Lemma 5.9** (cf. e.g. [17], Cor. 5.8). Let $F : E \to B$ be a Grothendieck opfibration between small categories, and let $C$ be cocomplete and locally small. Then the (point-wise) left Kan extension of a functor $G : E \to C$ along $F$ at $b \in \text{obj}(B)$ can be computed as a colimit over the fiber $F^{-1}(b)$,

$$ \text{Lan}_F G(b) \cong \text{colim}_{e \in F^{-1}(b)} G(e). \qquad (22) $$

To develop a variant and generalization of this result for G-relative opfibrations, let us first recall a few standard constructions and facts from category theory.

**Definition 5.10** ("Global" definition of left Kan extensions). Let $p : C \to C'$ be a functor, and $D$ a category. If $p^* := - \circ p : [C', D] \to [C, D]$ has a left adjoint $p'_1 : [C, D] \to [C', D]$, i.e., if $p'_1 \dashv p^*$, then for all functors $F : C \to D$ the left Kan extension $\text{Lan}_p F$ exists and is given by $\text{Lan}_p F = p'_1 F$.

**Lemma 5.11.** Let $L \dashv R$ be a pair of adjoint functors, with $L : C \to C'$ and $R : C' \to C$. Then for every category $D$, there is an induced pair of adjoint functors $- \circ R \dashv - \circ L : [C', D] \to [C, D]$. Therefore, for any functor $F : C \to D$, the left Kan extension $\text{Lan}_L F$ of $F$ along $L$ is given by $\text{Lan}_L F = F \circ R$.

**Theorem 5.12.** Let $F : E \to B$ be a G-relative opfibration for some wide subcategory G of B, and let $P : E \to \text{Set}$ be a covariant presheaf (for small categories E and B). Then for every object b of B, we find that

$$ \text{Lan}_F P(b) \cong \text{Lan}_{\pi_B} P \circ \pi_E(b) \cong \text{colim}_{(e,b,\gamma) \in \pi_B^{-1}(b)} P(e) \cong \left( \coprod_{e \in E} G(\bar{F}(e), \bar{b}) \times P(e) \right) / \sim_G . \quad (23) $$

Here, we used convenient shorthand notations $\bar{F}(e) := \iota^{-1} \circ F(e)$ and $\bar{b} := \iota^{-1}(b)$, and the equivalence relation $\sim_G$ is defined as

$$ \begin{gathered} (e, (\gamma, p)) \sim_G (e', (\gamma', p')) : \Leftrightarrow \exists e' - \varepsilon \to e' \in E, (\delta, q) \in G(\bar{F}(e'), \bar{b}) \times P(e) : \\ (\gamma, p) = (\delta \circ \iota^{-1} \circ F(\varepsilon) \circ \iota, q) \wedge (\gamma', p') = (\delta, P(\varepsilon)q). \end{gathered} \qquad (24) $$
17:16 Convolution Products on Double Categories and Categorification of Rule Algebras

The preceding discussion allows us to give a fully rigorous proof of Theorem 5.5, which may be found in the long version of the paper (to appear).

5.4 A brief analysis of unitality

As already mentioned, neither the framed bicategory Span nor the double category DPO modeling DPO-rewriting have the 0-CDP, in the sense that the functor $h_0 = U : D_0 \to D_1$ is not a globular opfibration. Nevertheless, the convolution product over DPO is in fact strongly unital. One way to establish unitality is by showing that DPO and similar double categories do satisfy a weakened version of the 0-CDP, equivalent to saying that $h_0$ is an opfibration relative to both the subcategory of S-vertical maps (i.e., double cells $\alpha$ such that $S(\alpha)$ is an identity in $D_0$) and the subcategory of T-vertical maps. We leave a more detailed analysis of this phenomenon to future work.

6 Categorification of rule algebras

As a presheaf, the convolution product $\hat{\Delta}_s * \hat{\Delta}_r$ of two representable presheaves $\hat{\Delta}_r$ and $\hat{\Delta}_s$ is isomorphic to a colimit of representables by general considerations on categories of presheaves. Moreover, the fact that the convolution product $*: \hat{\mathbb{D}} \times \hat{\mathbb{D}} \to \hat{\mathbb{D}}$ preserves colimits component-wise (Prop. 3.2) implies that it is entirely determined by its restriction $D_1 \times D_1 \to \hat{\mathbb{D}}$ to representable presheaves. In the introduction, we recalled how the rule algebra product was typically defined as a sum over admissible matchings between two rules, see equation (1). We now categorify this formula by showing that in many situations the convolution product of representable presheaves is isomorphic to a sum of representables of the following form

$$ \hat{\Delta}_{r_2} * \hat{\Delta}_{r_1} \cong \sum_{j \in J} \hat{\Delta}_{s_j} $$

where the family of horizontal cells noted

$$ r_2 \circled{\circled{r_1}} = (s_j : A_j \to B_j)_{j \in J} $$

can be effectively computed from $r_1$ and $r_2$. The property means that, in a certain sense, the family $r_2 \circled{\circled{r_1}} = (s_j)_{j \in J}$ classifies the convolution product of the presheaves $\hat{\Delta}_{r_2}$ with $\hat{\Delta}_{r_1}$, thus providing a categorified version of what is known as the concurrency theorem in rewriting theory (compare [1, 4, 5, 7, 13]). The intuition is that the composition of two rewrite rules can be classified into a number of different, disjoint cases, induced by all possible ways of matching the source of one rule with the target of the other.

In order to formalize this intuition in the language of double categories, we make from now on the assumption that our double category D satisfies the following property:

(i) the vertical category $D_0$ has multi-sums.

We find useful to recall at this stage the notion of *multi-sum* due to Diers [12]. Suppose that A and B are objects in a category. A *multi-sum* (or multi-coproduct) of A and B is a family of cospans

$$ (A \xrightarrow{a_i} U_i \leftarrow\limits_{b_i} B)_{i \in I} \qquad (29) $$

such that for any cospan $A \xrightarrow{f} X \xleftarrow{g} B$ there exists a unique $i \in I$ and a unique morphism $[f, g] : U_i \to X$ such that $f = [f, g] \circ a_i$ and $g = [f, g] \circ b_i$. The multi-sum generalizes
the standard notion of coproduct $A \xrightarrow{a} A + B \xleftarrow{b} B$ to situations in which there may not necessarily be a single universal cospan through which all other cospans $A \xrightarrow{f} X \xleftarrow{g} B$ factor, but there is nonetheless a universal family (29) of such cospans. As with the ordinary coproduct of two objects, when it exists the multi-sum of A and B is unique up to unique isomorphism.

**Notation:** given two horizontal 1-cells $r_1: A \to B$ and $r_2: C \to D$ of the double category $\mathcal{D}$, we find sometimes convenient to write $\Sigma^*_{(r_2, r_1)}$ for the set of cospans $(m_2, m_1) = (c_i, b_i)$ appearing in the multi-sum of B and C. This notation is used in particular in §6.2.

## 6.1 A first easy version of categorification

We start by establishing a categorification of equation (1) under the general assumption that (ii) the source and target functors $S, T: \mathcal{D}_1 \to \mathcal{D}_0$ are Grothendieck opfibrations.

This assumption holds for framed bicategories since it is weaker than the assumption that the pairing $(T, S)$ is an opfibration. It also holds for the double category TRS[$\Sigma$] of term rewriting which is not a framed bicategory. On the other hand, this assumption is too strong for the double category DPO, and we will see further below how to weaken it to prove a more general formula that also applies in that case. We establish that

**Theorem 6.1.** Assume $\mathcal{D}$ is a small double category satisfying assumptions (i) and (ii) and suppose that $r_1: A \to B$ and $r_2: C \to D$ are horizontal 1-cells in $\mathcal{D}$. In that case, the convolution product of two representable presheaves is isomorphic to the sum of representables

$$ \hat{\Delta}_{r_2} * \hat{\Delta}_{r_1} \cong \sum_{i \in I} \hat{\Delta}_{r_2 \langle c_i \rangle \diamond_i \langle b_i \rangle r_1} \qquad (30) $$

where the multi-sum of B and C is given by a family of cospans $(B \xrightarrow{b_i} U_i \xleftarrow{c_i} C)_{i \in I}$, and where $r_2 \langle c_i \rangle$ denotes the S-pushforward of $r_2$ along $c_i$ and $\langle b_i \rangle r_1$ denotes the T-pushforward of $r_1$ along $b_i$.

**Proof.** By definition, an element of $\hat{\Delta}_{r_2} * \hat{\Delta}_{r_1}$ evaluated at a generic horizontal 1-cell $r$ consists of three double cells of the following shape:

<figure><img src="image_11.png" /></figure>

Since $(B \xrightarrow{b_i} U_i \xleftarrow{c_i} C)_{i \in I}$ is the multi-sum of B and C, there exists a unique $i \in I$ and a morphism $[f, g]: U_i \to X$ such that $f = [f, g] \circ b_i$ and $g = [f, g] \circ c_i$. By the assumption that S and T are opfibrations, the double cells $\alpha_1$ and $\alpha_2$ therefore factor as follows:

<figure><img src="image_12.png" /></figure>
17:18 Convolution Products on Double Categories and Categorification of Rule Algebras

Observe that the double cell $(\tilde{\alpha}_2 \diamond_h \tilde{\alpha}_1) \diamond_v \beta$ is an element of the representable $\hat{\Delta}_{r_2 \langle c_i \rangle \diamond_h \langle b_i \rangle r_1}$ evaluated at $r$. This defines a natural transformation from $\hat{\Delta}_{r_2} * \hat{\Delta}_{r_1}$ to $\sum_{i \in I} \hat{\Delta}_{r_2 \langle c_i \rangle \diamond_h \langle b_i \rangle r_1}$, which is invertible by the universal properties of the multi-sum and the pushforward. ◀

**► Example 6.2.** In Example 3.3 we saw how the convolution product $\hat{\Delta}_r * \hat{\Delta}_r$ of the representable presheaf for the rewrite rule $r : m(e, x) \to x$ decomposes as the sum (9) of representables. This decomposition may be seen as a consequence of Theorem 6.1. First, note that the multi-sum of $x$ and $m(e, x)$ exists in $\text{TRS}[\Sigma]_0$, and is given by the minimal set of four unifying context/substitution pairs depicted below (with the last corresponding to the disjoint matching of the two terms, up to variable renaming).

<figure><img src="image_13.png" /></figure>

Moreover, observe that the functors $S, T : \text{TRS}[\Sigma]_1 \to \text{TRS}[\Sigma]_0$ are Grothendieck opfibrations, indeed even discrete opfibrations: the $S$-pushforward of a rule $t \to t'$ along a vertical 1-cell $t \to u = C[t\sigma]$ is the rule $C[t\sigma] \to C[t'\sigma]$, and similarly for the $T$-pushforward along a vertical 1-cell $t' \to u' = C[t'\sigma]$. Instantiating (30), we recover (9).

## 6.2 A more advanced version of categorification

In this subsection, we refine the assumptions of the previous subsection in order to establish in a more general framework that the convolution product of two representable presheaves is a sum of representables. One main motivation is to include among our examples the double category $\mathcal{DPO}$ and other double categories of interest in graph rewriting theory. From now on, we thus make the following two assumptions (iia) and (iib) on the double category $\mathcal{D}$, which generalize the assumption (ii) just made in the previous subsection:

(iia) the source functor $S : \mathcal{D}_1 \to \mathcal{D}_0$ is a multi-opfibration;

(iib) the target functor $T : \mathcal{D}_1 \to \mathcal{D}_0$ is a residual multi-opfibration.

The three assumptions (i), (iia) and (iib) are part of the definition of compositional rewriting double category (crDC) formulated in [5] where the interested reader will find the notion of (residual) multi-opfibration. We establish that

**► Theorem 6.3.** Assume $\mathcal{D}$ is a small double category satisfying assumptions (i), (iia) and (iib) and suppose that $r_1 : A \to B$ and $r_2 : C \to D$ are horizontal 1-cells in $\mathcal{D}$. In that case, the convolution product of two representable presheaves is isomorphic to the sum of representables

$$ \hat{\Delta}_{r_2} * \hat{\Delta}_{r_1} \cong \sum_{(m_2, m_1) \in \Sigma^*_{(r_2, r_1)}} \sum_{(m_1, j, \beta_{1,j}) \in T^*(r_1; m_1)} \sum_{\beta_{2,j,k} \in S^*(r_2, m_1, j, m_2)} \hat{\Delta}_{\beta_{2,j,k}(r_2) \diamond_h \beta_{1,j}(r_1)} \quad (31) $$

where $\Sigma^*_{(r_2, r_1)}$ denotes the set of cospans appearing in the multi-sum of $B$ and $C$, and where a choice of cleavages $S^*, T^*$ for $S, T$ on $\mathcal{D}_0$, respectively.
For illustration, every element of the presheaf $\hat{\Delta}_{r_2} * \hat{\Delta}_{r_1}$ at instance the horizontal arrow $r$ may be factored in the following way:

<figure><img src="image_14.png" /></figure>

where the pair $(m_2, m_1)$ of vertical arrows $m_1 : B \to U_i$ and $m_2 : C \to U_i$ is an element of the set $\Sigma^*_{(r_2, r_1)}$ of cospans appearing in the multi-sum of B and C.

# 7 Conclusion

In this paper, we explain how our original project of categorifying the rule algebra $(\mathcal{R}, \star)$ associated to a compositional rewriting theory brought us to formulate a very general notion of convolution product $*: \hat{\mathcal{D}} \times \hat{\mathcal{D}} \to \hat{\mathcal{D}}$ for vertical presheaves over a double category $\mathcal{D}$. The convolution product is only oplax associative in general, and we thus investigate in the paper sufficient conditions on the double category $\mathcal{D}$ for the convolution product to be strongly associative. We start by establishing that the convolution product is strongly associative in the case of framed bicategories, but not necessarily strongly unital. We then extend this result by formulating a more general cylindrical decomposition property for double categories (as an instance of the more general notion of relative opfibration) which, we show, implies that the convolution product is strongly associative under the assumption of $n$-CDP for all $n > 0$. The question of the strong unitality of the convolution product appears to be very subtle and interesting: it fails for the framed bicategory $\mathcal{Span}$ (Example 4.5), it holds for $\mathcal{TRS}[\Sigma]$ as a consequence of 0-CDP, and it holds for $\mathcal{DPO}$ despite the failure of 0-CDP.

One main achievement of the paper is to justify the view that the convolution product $*: \hat{\mathcal{D}} \times \hat{\mathcal{D}} \to \hat{\mathcal{D}}$ categorifies the product $*: \mathcal{R} \otimes_k \mathcal{R} \to \mathcal{R}$ of the rule algebra, thanks to formulas (30) and (31) which play the role of formula (1). We see this as a foundation for developing a deeper understanding of the rule algebra representation $\rho: \mathcal{R} \to \text{End}_{\mathcal{R}}(S)$ defined by formula (2) in the introduction, as well as formula (3). A strong benefit of categorification which we will clarify in future work is that it unifies, thanks to the Yoneda embedding, the rule algebra $\mathcal{R}$ with its action on states in $S$ through the representation $\rho$, following a healthy analogy with the well-known principle of Cayley theorem in algebra.

# References

1. Nicolas Behr. Sesqui-Pushout Rewriting: Concurrency, Associativity and Rule Algebra Framework. In *Proceedings of GCM 2019*, volume 309 of *EPTCS*, pages 23–52, 2019. doi:10.4204/eptcs.309.2.

2. Nicolas Behr. Tracelets and tracelet analysis of compositional rewriting systems. In *Proceedings of ACT 2019*, volume 323 of *EPTCS*, pages 44–71, 2020. doi:10.4204/eptcs.323.4.

3. Nicolas Behr, Vincent Danos, and Ilias Garnier. Stochastic mechanics of graph rewriting. In *Proceedings of LiCS '16*. ACM Press, 2016. doi:10.1145/2933575.2934537.
17:20 Convolution Products on Double Categories and Categorification of Rule Algebras

4 Nicolas Behr, Russ Harmer, and Jean Krivine. Concurrency theorems for non-linear rewriting theories. In Proceedings of ICGT 2021, volume 12741 of LNCS, pages 3–21. Springer, 2021. doi:10.1007/978-3-030-78946-6_1.

5 Nicolas Behr, Russ Harmer, and Jean Krivine. Fundamentals of Compositional Rewriting Theory, 2022. doi:10.48550/ARXIV.2204.07175.

6 Nicolas Behr and Joachim Kock. Tracelet Hopf Algebras and Decomposition Spaces (Extended Abstract). In Proceedings of ACT 2021, volume 372 of EPTCS, pages 323–337, 2022. doi: 10.4204/EPTCS.372.23.

7 Nicolas Behr and Jean Krivine. Compositionality of Rewriting Rules with Conditions. Com-
positionality, 3, 2021. doi:10.32408/compositionality-3-2.

8 Nicolas Behr, Jean Krivine, Jakob L. Andersen, and Daniel Merkle. Rewriting theory for the life sciences: A unifying theory of ctmc semantics. *Theoretical Computer Science*, 884:68–115, 2021.

9 Nicolas Behr and Paweł Sobocinski. Rule Algebras for Adhesive Categories (extended journal version). *LMCS*, Volume 16, Issue 3, 2020. doi:10.23638/LMCS-16(3:2)2020.

10 Andrea Corradini et al. Sesqui-Pushout Rewriting. In *Graph Transformations*, volume 4178 of LNCS, pages 30–45. Springer Berlin Heidelberg, 2006.

11 Brian Day. On closed categories of functors. In *Reports of the Midwest Category Seminar IV*, number 137 in Lecture Notes in Mathematics, pages 1–38, Berlin, Heidelberg, New York, 1970. Springer-Verlag.

12 Y. Diers. *Familles universelles de morphismes*, volume 145 of *Publications de l'U.E.R. mathématiques pures et appliquées*. Université des sciences et techniques de Lille I, 1978.

13 H. Ehrig et al. Fundamentals of Algebraic Graph Transformation. *Monographs in Theoretical Computer Science*, 2006. doi:10.1007/3-540-31188-2.

14 Niles Johnson and Donald Yau. *2-Dimensional Categories*. Oxford University Press, January 2021. doi:10.1093/oso/9780198871378.001.0001.

15 Saunders Mac Lane. *Categories for the Working Mathematician*, volume 5 of *Graduate Texts in Mathematics*. Springer New York, 2 edition, 1978. doi:10.1007/978-1-4757-4721-8.

16 Tom Leinster. *Higher Operads, Higher Categories*, volume 298 of *London Mathematical Society Lecture Note Series*. Cambridge University Press, 2004.

17 Paolo Perrone and Walter Tholen. Kan extensions are partial colimits. *Applied Categorical Structures*, 30(4):685–753, 2022. doi:10.1007/s10485-021-09671-9.

18 Michael Shulman. Framed bicategories and monoidal fibrations. *Theory and Applications of Categories*, 20(18):650–738, 2008.