Spans of cospans in a topos

TL;DR

This paper constructs a symmetric monoidal, compact closed bicategory of cospans in a topos, and demonstrates how double pushout rewriting rules can be represented within this framework, advancing categorical graph rewriting theory.

Contribution

It introduces a bicategory of monic spans of cospans in a topos, proving its symmetric monoidal and compact closed structure, and applies this to encode graph rewriting rules.

Findings

The bicategory is symmetric monoidal.

The bicategory is compact closed.

Double pushout rewrite rules can be encoded as 2-morphisms.

Abstract

For a topos $\mathbf{T}$, there is a bicategory $\mathbf{MonicSp(Csp(T))}$ whose objects are those of $\mathbf{T}$, morphisms are cospans in $\mathbf{T}$, and 2-morphisms are isomorphism classes of monic spans of cospans in $\mathbf{T}$. Using a result of Shulman, we prove that $\mathbf{MonicSp(Csp(T))}$ is symmetric monoidal, and moreover, that it is compact closed in the sense of Stay. We provide an application which illustrates how to encode double pushout rewrite rules as $2$-morphisms inside a compact closed sub-bicategory of $\mathbf{MonicSp(Csp(Graph))}$.