The n-Category Café

Let’s start with a simple example of a theory: the theory of monoids. This is a 1-theory, as you might guess from the fact that monoids form a 1-category. Each individual monoid (like $(\mathbb{N},+,0)$, for instance) is called a model of this theory; thus in general a 1-theory has a 1-category of models. More generally, we can define a monoid object in any category with finite products (say); thus a 1-theory has a 1-category of models internal to any sufficiently structured 1-category.

So far so good, but what exactly is a 1-theory in general? As discussed in this post and its comments, there are several “levels of realization” at which we might consider a theory, but for now I want to focus on the two extreme ends: the fully syntactic and the fully semantic. In a fully syntactic presentation, the theory $T_{Mon}$ of monoids looks like this:

• One generating type $M$.
• Two generating terms $(x:M), (y:M) \vdash (m(x,y) : M)$ and $\vdash (e:M)$.
• Three generating equalities $(x:M),(y:M),(z:M) \vdash (m(m(x,y),z) = m(x,m(y,z)) : M)$ and $(x:M) \vdash (m(x,e)=x : M)$ and $(x:M) \vdash (m(e,x)=x : M)$.

The fully semantic presentation of the theory of monoids is its Lawvere theory $L_{Mon}$ or walking model: the category with finite products freely generated by a monoid object $M$. This has the universal property that for any category $C$ with finite products, functors $L_{Mon}\to C$ that preserve finite products are equivalent to monoid objects in $C$.

The connection between the syntactic and semantic presentations is the following:

• The objects of $L_{Mon}$ are the types obtained by starting with the generating type and freely adding finite product types $A\times B$ and the nullary product $1$.
• The morphisms of $L_{Mon}$ are represented by the terms obtained by starting with the generating terms $m(x,y)$ and $e$ and allowing arbitrary substitutions for variables (i.e. composites of morphisms), such as $m(m(x,x),m(y,m(z,y)))$.
• These terms are then quotiented by the congruence generated by the generating equalities of associativity and unitality.

(The intermediate stages of “realization” I referred to are what you get by, e.g., closing up the generating equalities into a congruence but retaining the special status of the generating terms $m(x,y)$ and $e$, and similarly for other places of drawing the line. I want to ignore these not just for expositional clarity, but because when you get to dependent type theory it’s no longer clear to me that there is anywhere “in the middle” to draw the line; see here.)

Now we can say more generally what a 1-theory is (at least, one kind of 1-theory). A syntactic 1-theory has a set of generating types, a set of generating terms (which may involve not only the generating types but those obtained from them by applying finite products), and a set of generating equalities (which may involve not only the generating terms but those obtained from them by substitutions). And a semantic 1-theory is just a category with finite products. Every syntactic 1-theory generates a semantic 1-theory, which is “freely generated by a model”. And every semantic 1-theory can be generated by at least one syntactic 1-theory, such as the “tautological” one whose generating types are all the objects, whose generating terms are all the morphisms, and whose generating axioms are all the equalities. (I’m not being precise about any of this, but it can be made precise.)

[A brief digression]: Note that a given semantic 1-theory can have many different syntactic presentations. For instance, the semantic 1-theory of monoids can be presented either as above in “biased” form with one binary and one nullary operation, or in an “unbiased” form with one $n$-ary operation for all $n$ (and also in many other ways). Nevertheless, the relationship between syntax and semantics is often formulated as an equivalence of categories. Personally, I’m not as fond of such formulations, because in order to make them true one has essentially to define “morphisms of syntactic theories” just so as to make such an equivalence hold, rather than in the “natural” way consisting of functions between the generating types, generating terms, and generating axioms. It’s certainly important that the biased notion of monoid agrees with the unbiased version, but I think it’s also important that the two notions are different in some sense, and to me the natural way to express this is to say that they are two different syntactic theories that generate the same semantic theory. [End of digression]

Now, so far, all of this is only about “finite-product 1-theories”: the syntactic types are generated only by the finite-product constructors $A\times B$ and $1$, the semantic theories are categories with finite products, and the internal models likewise happen in categories with finite products. The notion such as “category with finite products” that we fix in order to give rise to this whole structure is sometimes called its doctrine.

We can then consider other doctrines, such as “monoidal categories”. In this doctrine, the internal models happen in monoidal categories, the semantic theories are monoidal categories, and the syntactic types are generated by tensor product constructors $A\otimes B$ and $I$. In a much more highly structured doctrine like “locally cartesian closed categories” or “toposes”, the semantic theories are such categories, and the syntactic types are generated by higher-order constructors such as dependent products, power-types, universes, and so on. Each choice of doctrine determines a notion of “syntactic 1-theory in that doctrine”, a notion of “semantic 1-theory in that doctrine”, and the above sort of relation between them.

But, how do we define a “doctrine” in general? We have lots of examples, but without a general structure for them we have to develop the general theory for each such doctrine separately. This is clearly an undesirable state of affairs.

Along the way to answering this question, note first that the semantic 1-theories in any doctrine form a 2-category — for instance, the 2-category of categories with finite products, or the 2-category of monoidal categories, or the 2-category of toposes. Thus, it is natural to guess that a doctrine will be a sort of “2-theory” which has a 2-category of “models”, and that these models coincide with semantic 1-theories in that doctrine/2-theory. We might even leap to a general principle such as:

The models of an $(n+1)$-theory are the semantic $n$-theories in that $(n+1)$-theory (regarded as an “$n$-doctrine”, i.e. a language in which to write $n$-theories).

To see whether this makes sense, let’s do a bit of negative thinking. In what sense can we consider the models of a 1-theory as “semantic 0-theories”? In particular, what is a syntactic 0-theory?

Well, note that a syntactic 1-theory can be regarded as a kind of presentation of a semantic 1-theory: we specify the generating objects, generating morphisms, and relations that they have to satisfy. So a syntactic 0-theory should be a suitable kind of presentation of a semantic 0-theory, i.e. of a model.

For instance, in the 1-theory (= 0-doctrine) of monoids, a syntactic 0-theory is a monoid presentation: a set of generating elements together with relations between formal products of generators. Every monoid presentation $(G, R)$ presents a monoid $L_{G,R}$ in the usual way, i.e. every syntactic 0-theory gives rise to a semantic 0-theory. Moreover, this presented monoid has a universal property: monoid homomorphisms $L_{G,R} \to M$, for any monoid $M$, are equivalent to “internal models” of $(G,R)$ in $M$, i.e. interpretations of each generator $x\in G$ as an element of $M$ such that the relations in $R$ hold in $M$.

Note that although we are speaking of internal models of a syntactic 0-theory in an arbitrary semantic 0-theory (in the same 0-doctrine = 1-theory), these semantic 0-theories are not themselves arbitrary internal models of the 1-theory in question, but specifically models in the “canonical” 1-category $Set$. Thus our principle above should really be refined a bit to

The models of an $(n+1)$-theory in the $(n+1)$-category $n Cat$ are the semantic $n$-theories in that $(n+1)$-theory.

How low can we go? Well, the canonical 0-category is $(-1)Cat$, i.e. the (po)set $\Omega$ of truth values. This is, indeed, a monoid under the operation “and” (the decategorification of the cartesian product in $Set$). Thus, given a 0-theory $M$ (a monoid), the semantic $(-1)$-theories in $M$ (regarded as a $(-1)$-doctrine) are the models of $M$ in $(-1)Cat$, i.e. the monoid homomorphisms $M\to \Omega$.

Since $\Omega$ is the subobject classifier (in $Set$), a function $M\to \Omega$ is the same as a subset of $M$. And asking that such a function is a monoid homomorphism says precisely that this subset is a submonoid, i.e. contains the identity element $e\in M$ and is closed under the multiplication. Thus, the semantic $(-1)$ theories in the 0-theory $M$ are the submonoids of $M$; a statement which, if not obviously correct, is at least not obviously incorrect. [Edit: A commenter points out below that this is wrong: there is an extra condition on such submonoids.]

(As usual, the ladder bottoms out here: the “canonical” $(-1)$-category is $(-2)Cat$, namely the truth value “true”, which is the terminal object; thus there are no nontrivial $(-2)$-theories.)

Since negative thinking seems to justify our principle, let’s go back to climbing upwards: what is a 2-theory? We should expect to have both syntactic and semantic 2-theories. A semantic 2-theory will be, in particular, a 2-category, just as a semantic 1-theory (e.g. a Lawvere theory) is, in particular a 1-category. But it will be a structured 2-category, and a syntactic 2-theory will be a way of “presenting” such a structured 2-category in terms of generating objects, morphisms, 2-morphisms, and relations.

What kind of 2-categorical structure will semantic 2-theories have? Well, that depends on the 3-theory in which they live. (-: (-: (-:

The simplest thing to do would be to categorify our running example. In this case, the 3-theory would have as its models (in $2 Cat$) 2-categories with finite products. These are then the semantic 2-theories in this 3-theory (= 2-doctrine). And a syntactic 2-theory in this 3-theory is a presentation of a particular such 2-category.

Below we’ll mention some other possible 3-theories, but first I want to talk some more about syntax. So far, this discussion has been mainly semantic, with comments about the syntax limited to the vague term “presentation”. But we can be more explicit about what the syntax looks like, especially when we consider varying two adjacent levels simultaneously, such as $n=1$ and $n=2$.

A particular 2-theory specifies the “doctrine” in which we write 1-theories, which syntactically means the rules of the deductive system in which we formulate those 1-theories. For instance, the 2-theory of “categories with finite products” specifies rules like

$$\frac{A \; type \qquad B \;type}{A\times B \; type}$$

saying that we can form cartesian product types, together with their usual introduction/elimination/computation rules, for instance the pairing rule

$$\frac{\Gamma\vdash a:A \qquad \Gamma \vdash b:B}{\Gamma\vdash (a,b) :A\times B}$$

A particular 1-theory in this doctrine, on the other hand, specifies generating types, terms, and axioms without varying the rules. The theory of monoids, the theory of groups, the theory of rings, the theory of a module over a ring, and so on — all of these can be specified by generating types, terms, and axioms without varying the rules about finite product types.

A different 2-theory specifies a different doctrine, with corresponding different rules. For instance, the 2-theory of “symmetric monoidal categories” specifies rules like

$$\frac{A \; type \qquad B \;type}{A\otimes B \; type}$$

for tensor product types, together with different introduction/elimination/computation rules, such as a “linear” pairing rule

$$\frac{\Gamma\vdash a:A \qquad \Delta \vdash b:B}{\Gamma,\Delta\vdash (a,b) :A\otimes B}$$

This corresponds to tensoring together two morphisms with different domains and codomains (the comma in “$\Gamma,\Delta$” is a “judgmental” version of the tensor product $\otimes$), in contrast to how the pairing rule of cartesian products uses the universal property for a pair of morphisms with the same domain.

We can then formulate particular 1-theories in this doctrine, such as the theories of monoids, comonoids, bimonoids, Hopf algebras, etc. — but not the theories of groups or rings, since these require duplication of variables. (Note that the “same” theory of monoids can be formulated in both doctrines. Indeed, the theory of monoids in the doctrine of finite products is “freely extended” from the theory of monoids in the doctrine of monoidal categories. This sort of “change of doctrine” is another interesting direction to think about, but tangential to the point for now.)

Now I think we can see the last point I mentioned before the fold about the ambiguity in the noun phrase “type theory”. Sometimes when people say “theory” they mean something like the theory of monoids, i.e. a 1-theory consisting (syntactically) of generating types, terms, and axioms. For instance, when people say things like “the 2-category of Martin-Löf type theories is equivalent to the 2-category of locally cartesian closed categories”, they mean “type 1-theories”. But other times when people say “type theory” they are referring to a 2-theory, consisting (syntactically) of rules: for instance, the phrase “Martin-Löf type theory” (singular) has this meaning.

Similarly, the phrase “internal language” sometimes refers to the “tautological” syntactic 1-theory associated to a semantic 1-theory, e.g. “the internal language of the category of reflexive graphs” is a particular 1-theory with one generating type for each reflexive graph, etc.. But other times the phrase “internal language” is used to indicate a particular syntax/semantics adjunction, e.g. “extensional Martin-Lof type (2-)theory is an internal language for locally cartesian closed categories”.

So far so good… but unfortunately the world of syntax is not so simple. Even once we’ve fixed a particular doctrine, there can be many different ways to write down rules in which to formulate syntactic theories. In other words, it’s not really quite right to say that an $(n+1)$-theory specifies the rules for a deductive system for $n$-theories; it’s more correct to say that it specifies the intended categorical structure that such rules should represent. (A syntactic $(n+1)$-theory gives a bit more information than a semantic one here, but still not enough.)

My favorite simple example of this is 0-theories in the 1-theory of monoids (so $n=0$). The 1-theory of monoids specifies the intended structure on a set that a “deductive system for monoids” should represent — namely, a monoid structure. What is a “deductive system for monoids”? Roughly speaking, it’s a method of starting from a monoid presentation $(G,R)$ and generating the entire monoid. We have to first produce a collection of “words” from the generating elements $g$, and then quotient them by the specified relations $R$ as well as the monoid axioms. But what is a “word”? There are many possible answers; here are a few:

1. A word is a finite list of generating elements, like $a b c d$.
2. A word is a finite list of generating elements bracketed in binary and nullary groups, such as $(a b)((()c)d)$.
3. A word is a finite list of generating elements bracketed in groups of arbitrary arity, such as $(a b c)()(d)$.

Answer #1 is, of course, the simplest, and the one we normally use. But answer #3 is all we can produce “naturally” if we start from the semantic 1-theory of monoids, which has exactly one operation of each arity. If we start instead from the “biased” syntactic 1-theory of monoids, which has one binary and one nullary generating term, we can obtain answer #2. Answer #1 involves some deeper analysis of the notion of monoid, since it already incorporates the associativity axiom rather than imposing it afterwards as part of the quotienting. (The proof that answer #1 actually works is, essentially, a form of “cut-elimination”.) Note also that the choice of “notion of word” actually already has to be made before we specify the entire presentation $(G,R)$, since each relation in $R$ has to relate a pair of words.

Similarly up a level, once we fix a 2-theory, there are many different deductive systems that can present 1-theories in that doctrine. For instance, cartesian closed categories can be presented using lambda-calculus, but also combinatory logic. Monoidal categories can be presented as I described above using “intuitionistic linear type theory”, but also a “combinatory” version as in the rosetta stone paper, and even string diagram calculus can be regarded as a way to present monoidal categories.

Any such deductive system has advantages and disadvantages. However, for the purposes of computation — and also, arguably, for the purposes of informal usage as a foundation for mathematics, although that’s a discussion I don’t have space for right now — it’s important to look for a particular collection of advantages, notably the “admissibility” of operations such as cut and substitution, and computational properties such as normalization and canonicity. These sorts of metatheorems are what type theorists spend a lot of their time proving — about each doctrine separately.

Now I can finally describe the programme that Dan, Mitchell, and I are undertaking. Given a particular 3-theory, we aim to describe a particular deductive system for syntactic 2-theories in that 3-theory, and associate to any such syntactic 2-theory $D$ a specific deductive system for syntactic 1-theories in $D$, such that the latter (1) indeed has the correct semantics, i.e. it presents the correct semantic 1-theories, and (2) has the good meta-theoretic properties that type theorists want, such as cut-elimination, normalization, and canonicity. For a particular syntactic 1-theory, the deductive system that we get is not usually identical to any existing deductive system for that 1-theory, but it is almost always related to it by a fairly direct translation (in general, rules of the existing system tend to translate into the successive applications of two or more “more basic” rules in our system).

To the extent that it succeeds, this has the potential to simplify our lives considerably: instead of treating each 2-theory separately, we can obtain them all automatically from a general theorem. Or, rather, from a small collection of general theorems, because (for the present, and also the foreseeable immediate future) we are treating each 3-theory separately.

• The first paper by Dan and myself dealt with the 3-theory of (totally unstructured) 2-categories. Syntactically, this corresponds to “unary type (2-)theories” with judgments such as $x:A \vdash b:B$ with exactly one type to both the left and the right of the turnstile.
• The second paper, with Dan and Mitchell, dealt with the 3-theory of cartesian monoidal 2-categories (actually, for technical reasons we used cartesian 2-multicategories). Syntactically, this corresponds to “simple type (2-)theories” with judgments such as $x:A, y:B, z:C \vdash d:D$ with a finite list of types to the left but exactly one type to the right, and no dependent types.
• At the end of my HoTTEST talk, I reported on our current progress towards a 3-theory that corresponds syntactically to “dependent type (2-)theories”. The semantic version of this seems to be some kind of “comprehension 2-category”.

These three 3-theories are “cumulative”, i.e. any 2-theory in one of the first two can also be formulated in the more expressive ones below it, in the same way that the theory of monoids in the doctrine of monoidal categories can also be formulated in the more expressive doctrine of categories with finite products. So once our current work on dependent type 2-theories is complete, it will (to a certain extent) subsume the previous two papers. However, there are also other 3-theories that remain to be studied. Some, such as the 3-theory of first-order logic, live in between the 3-theories of simple type 2-theory and dependent type 2-theory. But another notable one is:

• There should be a 3-theory that corresponds syntactically to “classical simple type (2-)theories” with judgments such as $A,B,C \vdash D,E$ that allow finite lists of types on both sides of the turnstile. For instance, the 2-theory of $\ast$-autonomous categories (classical linear logic), and also of Boolean algebras (classical nonlinear logic), live in this 3-theory.

We have some ideas about this latter 3-theory, but it’s still rather up in the air. It should subsume the 3-theory of simple type 2-theories, but is incomparable with the 3-theory of dependent type 2-theories (neither subsumes the other), and it’s unclear to me whether there is any 3-theory that subsumes both of them.

Since this is the $n$-Category Café, someone is going to ask the question “what about 4-theories?” or even “what about $\infty$-theories?”, so let me go ahead and answer it preemptively.

In principle, the sort of “interaction between adjacent levels” that we’re interested in — using a 2-theories in a particular 3-theory to describe a deductive system for syntactic 1-theories in such 2-theories — could be generalized to any adjacent levels. For instance, we could imagine using 7-theories in a particular 8-theory to describe a deductive system for syntactic 6-theories in such 7-theories. However, in practice, when dimensions get beyond 2 or 3, human beings seem to do better with some sort of “encoding” of the higher-dimensional structure in terms of lower-dimensional structure.

Homotopy type theory is a good example: despite being ostensibly a theory of $(\infty,1)$-categories, as a type theory it is actually just a 2-theory, or a deductive system for a certain class of 1-theories. Syntactically, this is roughly because it doesn’t include any basic 2-cell judgments; its 2-cells and higher cells are all encoded implicitly using 1-morphisms into path objects. Semantically, this corresponds to the fact that its most “direct” notion of model is actually a kind of structured 1-category (a comprehension category, category with families, etc.); a coherence theorem then (hopefully) relates these to the intended $(\infty,1)$-categorical models.

So, while in principle one could go on to talk about 4-theories, $n$-theories, and $\infty$-theories, it’s not clear to me that anyone will.

To conclude, let me say a bit about how this project relates to modal logic. In a syntactic 2-theory with multiple generating types, the objects of the resulting semantic 2-category are not single structured categories, but diagrams of several categories with functors and natural transformations between them. Thus, the corresponding syntactic 1-theories have several “classes” of types, one for each category. These classes of types are generally called “modes”, type theory or logic with multiple modes is called “modal”, and the functors between these categories are called “modalities”. Thus, modal logics are particular 2-theories, to which our framework applies.

Traditional modal logic involves “logical” modalities such as $\Box$ (“it is necessary that…”) and $\lozenge$ (“it is possible that…”). More recently, in cohesive type theory (first here) we have introduced modalities denoted $ʃ,\flat,\sharp$ that correspond to the monads and comonads on a cohesive topos. Other applications have also appeared or are in the works, such as this paper on internal universes, a type theory for parametrized spectra involving a self-adjoint modality $\natural$, and a type theory for “differential cohesion” involving six modalities $ʃ,\flat,\sharp,\Re,\Im,\&$. I fully expect that in the future such modal type theories will proliferate, so having a general framework to produce them will be very useful.