Table of Contents
Fetching ...

Distributive laws for Lawvere theories

Eugenia Cheng

Abstract

Distributive laws give a way of combining two algebraic structures expressed as monads; in this paper we propose a theory of distributive laws for combining algebraic structures expressed as Lawvere theories. We propose four approaches, involving profunctors, monoidal profunctors, an extension of the free finite-product category 2-monad from Cat to Prof, and factorisation systems respectively. We exhibit comparison functors between CAT and each of these new frameworks to show that the distributive laws between the Lawvere theories correspond in a suitable way to distributive laws between their associated finitary monads. The different but equivalent formulations then provide, between them, a framework conducive to generalisation, but also an explicit description of the composite theories arising from distributive laws.

Distributive laws for Lawvere theories

Abstract

Distributive laws give a way of combining two algebraic structures expressed as monads; in this paper we propose a theory of distributive laws for combining algebraic structures expressed as Lawvere theories. We propose four approaches, involving profunctors, monoidal profunctors, an extension of the free finite-product category 2-monad from Cat to Prof, and factorisation systems respectively. We exhibit comparison functors between CAT and each of these new frameworks to show that the distributive laws between the Lawvere theories correspond in a suitable way to distributive laws between their associated finitary monads. The different but equivalent formulations then provide, between them, a framework conducive to generalisation, but also an explicit description of the composite theories arising from distributive laws.

Paper Structure

This paper contains 8 sections, 32 theorems, 97 equations.

Key Result

Proposition 1.8

Given a monad $T$ on $\textrm{\bfseries {\upshape {Set}}}$ we can construct a Lawvere theory $\mathbb L_T$ as the full subcategory of $\hbox{\bfseries {\upshape {Kl} }} T^{\space\textrm{\upshape{op}}}$ whose objects are those of $\mathbb F$. Moreover if $T$ is finitary

Theorems & Definitions (71)

  • Definition 1.1
  • Remark 1.2
  • Definition 1.3
  • Example 1.4
  • Remark 1.5
  • Definition 1.6
  • Example 1.7
  • Proposition 1.8
  • Remark 1.9
  • Proposition 1.10
  • ...and 61 more