Functorial Semantics for Relational Theories

TL;DR

This paper extends Lawvere's functorial semantics to Frobenius theories, enabling models in categories of relations and cartesian bicategories, broadening the scope of categorical universal algebra.

Contribution

It introduces Frobenius theories as a generalization of Lawvere theories, allowing models in relational and bicategorical contexts.

Findings

Frobenius theories generalize Lawvere theories to relations.

Models can be interpreted in cartesian bicategories.

The framework broadens categorical universal algebra applications.

Abstract

We introduce the concept of Frobenius theory as a generalisation of Lawvere's functorial semantics approach to categorical universal algebra. Whereas the universe for models of Lawvere theories is the category of sets and functions, or more generally cartesian categories, Frobenius theories take their models in the category of sets and relations, or more generally in cartesian bicategories.