The Azimuth Project
The Syntax of Coherence (Rev #2)

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