Universal Constructions for (Co)Relations: categories, monoidal categories, and props

TL;DR

This paper provides a unified, modular framework for understanding categories of relations and corelations used in string diagram semantics, simplifying axiomatisation and connecting diverse fields like quantum computing and control theory.

Contribution

It characterizes semantic categories of relations and corelations as colimits of simpler categories, unifying various existing theorems and aiding in axiomatisation.

Findings

Semantic categories as colimits of simpler categories

Unified framework for relations and corelations

Simplifies axiomatisation of string diagram semantics

Abstract

Calculi of string diagrams are increasingly used to present the syntax and algebraic structure of various families of circuits, including signal flow graphs, electrical circuits and quantum processes. In many such approaches, the semantic interpretation for diagrams is given in terms of relations or corelations (generalised equivalence relations) of some kind. In this paper we show how semantic categories of both relations and corelations can be characterised as colimits of simpler categories. This modular perspective is important as it simplifies the task of giving a complete axiomatisation for semantic equivalence of string diagrams. Moreover, our general result unifies various theorems that are independently found in literature and are relevant for program semantics, quantum computation and control theory.