# The Azimuth Project The Syntax of Coherence (changes)

Showing changes from revision #2 to #3: Added | Removed | Changed

## 2-theories and 2-algebras

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

Let $\mathsf{Fin}_{sk}$ denote a skeleton of the category of finite sets and functions. Let $\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 $T$ with a given coproduct structure and a 2-functor $G_T \colon \overline{\mathsf{Fin}}_{sk} \to T$ such that $G_T$ is bijective on 0-cells and preserves the coproduct structure.

## Examples

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

• Let $T_{Mon}$ denote the theory of monoidal categories?, which has non-trivial generating 1-cells $\otimes \colon 1 \to 2$ and $e \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.”