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.


  • Fin¯ sk\overline{Fin}_{sk} itself is the theory of categories, or of just objects.

  • Let T MonT_{Mon} denote the theory of monoidal categories?, which has non-trivial generating 1-cells :12\otimes \colon 1 \to 2 and e:10e \colon 1 \to 0 and 2-cells α\alpha, λ\lambda, and ρ\rho as in the definition of monoidal categories, satisfying the equations you would expect.

  • Similarly, there is a 2-theory for braided monoidal categories?, balanced monoidal categories?, and symmetric monoidal categories?.

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.”