The Azimuth Project
The Syntax of Coherence

2-theories and 2-algebras

The main thing I need out of this paper is examples of 2-theories.

Let Fin sk\mathsf{Fin}_{sk} denote a skeleton of the category of finite sets and functions. Let Fin¯ sk\overline{Fin}_{sk} denote the 2-category with the same 0-cells and 1-cells, and only identity 2-cells.

Definition A (single-sorted algebraic) 2-theory is a 2-category TT with a given coproduct structure and a 2-functor G T:Fin¯ skTG_T \colon \overline{\mathsf{Fin}}_{sk} \to T such that G TG_T is bijective on 0-cells and preserves the coproduct structure.


Kronecker product

In section 4, a tensor product of 2-theories is defined (Definition 6).

Future work

“There are many different directions in which this work can be extended. An obvious generalization is multi-sorted 2-theories. More to the point, however, would be 2-theories whose 0-cells are the free monoid on two generators λ and ρ corresponding to covariance and contravarience. We may call such 2-theories “bi-sorted 2-theories”. Models/algebras of such theories will be in a 2 category C that has both a product structure and an involution (?)op. The prototypical example of such a category is Cat. Algebras of these theories would be functors that take λ to c and ρ to (c) op. Using such a formalism, would help us understand the many structures that demand contravarient functors.”