Double Categories – jackswebsite

Introduction

A double category has both: tight arrows (functions), loose arrows (relations), and squares relating them. We use these to express how to lift programs (or functions) to specifications (or relations) of their behavior.

This is a reference for effectful programs as arrows Power and Robinson (1997).

Double categories

Definition 1 A proto double category has objects, tight arrows $f : V \to V'$, loose arrows $M : V \not\rightarrow W$ and squares

$\begin{tikzcd} V && W \\ & {\Downarrow \phi} \\ V' && W' \arrow["N"{inner sep=.8ex}, "\shortmid"{marking}, from=1-1, to=1-3] \arrow["f"', from=1-1, to=3-1] \arrow["g", from=1-3, to=3-3] \arrow["N'"'{inner sep=.8ex}, "\shortmid"{marking}, from=3-1, to=3-3] \end{tikzcd}$

with loose composition associative and unital up to coherent (globular) isomorphisms.

Definition 2 A double category is a proto double category which furthermore has a loose composition of squares

$\begin{tikzcd} V && W && X \\ & {\Downarrow \phi} && {\Downarrow \psi} \\ {V'} && {W'} && {X'} \arrow["N"{inner sep=.8ex}, "\shortmid"{marking}, from=1-1, to=1-3] \arrow["f"', from=1-1, to=3-1] \arrow["M"{inner sep=.8ex}, "\shortmid"{marking}, from=1-3, to=1-5] \arrow["g"', from=1-3, to=3-3] \arrow["h"', from=1-5, to=3-5] \arrow["{N'}"'{inner sep=.8ex}, "\shortmid"{marking}, from=3-1, to=3-3] \arrow["{M'}"'{inner sep=.8ex}, "\shortmid"{marking}, from=3-3, to=3-5] \end{tikzcd}$

as well as tight composition of squares

$\begin{tikzcd} V && W \\ & {\Downarrow \phi} \\ V' && W'\\ & {\Downarrow \phi'}\\ V'' && W''. \\ \arrow["N"{inner sep=.8ex}, "\shortmid"{marking}, from=1-1, to=1-3] \arrow["f", from=1-1, to=3-1] \arrow["g", from=1-3, to=3-3] \arrow["N'"'{inner sep=.8ex}, "\shortmid"{marking}, from=3-1, to=3-3] \arrow["f'", from=3-1, to=5-1] \arrow["g'", from=3-3, to=5-3] \arrow["N''"'{inner sep=.8ex}, "\shortmid"{marking}, from=5-1, to=5-3] \end{tikzcd}$

which satisfy the interchange law.

Examples

Example 1 $\mathbb{R}\text{el}$ has sets, functions and relations $R \subseteq A \times B$. A square from $R$ to $R'$ along $f, g$ exists when

\[\forall (x, y) \in R.\ (f(x), g(y)) \in R'.\]

Example 2 $\mathbb{P}\mathbb{R}\text{el}$ has sets, functions and proof relevant relations $R : A \not\rightarrow B$ (functor $\text{Disc}(A) \times \text{Disc}(B) \rightarrow \mathcal{S}\text{et}$). A square from $R$ to $R'$ along $f$ and $g$ is a $\phi =$

\[(\phi_{x,y} : R(x,y) \rightarrow R'(f(x),g(y)))_{(x,y) \in A \times B}.\]

Example 3 For a symmetric monoidal category $\mathcal{V}$, $\mathcal{V}-\mathbb{P}\text{rof}$ has $\mathcal{V}$-enriched categories, $\mathcal{V}$-enriched functors and $\mathcal{V}$-Profunctors $M : \mathbb{A}\not\rightarrow\mathbb{B}$ ($\mathcal{V}$-functor $\mathbb{A} \otimes \mathbb{B}^{op} \rightarrow \mathcal{V}$). A square from $M$ to $M'$ along $F$ and $G$ is a $\mathcal{V}$-natural transformation

\[\phi : M \Rightarrow M' \circ F \otimes G^{op}.\]

Results

Pending

References

Power, John, and Edmund Robinson. 1997. “Premonoidal Categories and Notions of Computation.” Mathematical Structures in Computer Science 7 (5): 453–68.

PDF