The doctrine of computational trinitarianism implies that there should be a categorial analogue of two-dimensional type theory … and indeed there is. It is called, oddly enough, two-dimensional category theory, which arose first for numerous reasons. What is two-dimensional category theory? And how does it relate to two-dimensional type theory?

Two-dimensional category theory may be seen as an instance of the general concept of *enriched *categories in which the collection of morphisms between any two objects is endowed with some additional structure. A *locally small* category is one for which the maps between any two objects form a set, called the *hom set*. An *order-enriched* category is one in which the morphisms form an ordered set, which is a set equipped with a pre-order (reflexive and transitive relation) on maps such that composition is monotone. Order-enriched categories were used by Mitchell Wand and Gordon Plotkin and Mike Smyth in their development of the category-theoretic interpretation of recursive types. Specifically, an *O-category* is an order-enriched category whose objects are cpo’s (pre-orders closed under sup’s of chains, and hence containing a least element) and whose hom sets are themselves cpo’s and for which composition is continuous (monotone and preserves suprema of chains).

More generally still, one may consider (different forms of) *category-enriched* categories, in which the hom sets are structured as categories with their own* vertical *notion of identity and composition that meshes well with the *horizontal* notion of identity and composition of the category itself. (I will not give here the precise meaning of “meshes well with”, since there are several possible notions and I will be discussing this structure in the type-theoretic setting below.) The vertical maps are *maps between maps* that can be interpreted in several ways. One way is as “witnesses” to an ordering relation among maps, viewing a category as a “pre-order with witnesses”, perhaps an approximation relation among maps such as arises in domain theory. Another is to view these maps as homotopies between continuous functions on a space; these are the continuous deformations of one map into another. (This is usually expressed by introducing a “time” coordinate ranging over the unit interval, and stating that a homotopy *h* between maps *f *and *g* is a continuous mapping such that at time zero *h* agrees with *f*, at time 1 agrees with *g*, and smoothly varies at times between.) An important special case of category-enriched categories are those whose morphisms form (not just a category but also) a *groupoid*, a category in which each map is invertible. These can be thought of as “equivalence relations with evidence”; the vertical maps are “proofs” that two horizontal maps are equivalent (for example, homotopic).

The sort of category-enriched categories that I have in mind are called *(strict)* *2-categories*. And as the terminology suggests, there is nothing special about the number 2 here; one can consider -categories for any number , and even -categories that incorporate all of these into one grand structure (strictly or weakly). To help manage this structure, the categorists have a uniform terminology that I wish to introduce here, called *cells*. The objects in a category are the *0-cells*, the maps are the *1-cells*, the maps between maps (transformations, homotopies, …) are the *2-cells*, and so forth. A 2-category is one for which we stop at 2-cells; all higher cells being degenerate and hence ignored. Often the 2-cells (and higher) form groupoids (in one of two senses that I will come back to later); a (2,1)-category is a 2-category in which the 2-cells form a groupoid (but the 1-cells need only form a category). The class of -categories are the subject of intense interest these days, in part because of their importance in homotopy theory. They are, however, notoriously hard to manage, and, from what I understand, it is not yet clear what is even the correct definition.

Returning to two-dimensional type theory, and applying the types-as-categories correspondence, we get that types are 0-cells, terms (with free variables) are 1-cells, and transformations are 2-cells. General terms are not invertible, but transformations are, giving rise to a (strict) groupoid structure expressed by the judgement . The rules for composition of transformations expresses the vertical structure as forming a strict groupoid. Ordinary substitution expresses the horizontal structure of terms as maps (plugging in terms for free variables). But how do these interact? In strict two-dimensional type theory this interaction is expressed by definitional equalities that express the *interchange law* between horizontal and vertical composition. Specifically, we have the following rule:

(More generally one must consider arbitrary contexts, and transformations between substitutions, but this instance of the general case expresses the essential idea.)

This “substitution” principle must satisfy some equational laws that amount to the following conditions:

- Identity: .
- Composition: .
- Interchange: .
- Delegation: .

(Here is the application of a transformation to a term; it is there to “get the types right”.) The interchange law is the type-theoretic analogue of the required interaction between 1-composition and 2-composition in a (strict) 2-category.

This is the judgmental structure of strict two-dimensional type theory. There are several directions we can go from here. One is to clarify the strict/weak distinction that has been underlying our discussions so far. Another is to consider how to extend this to three- and higher-dimensional (or, dare I say it, infinite-dimensional) type theory. The crucial ingredient for both of these discussions is one particular type constructor (more precisely, family of type constructors) that *internalizes* the hom structure as a type. In the groupoidal case, where the higher structure is symmetric (invertible), this corresponds to (a version of) the Martin-Löf identity type. The introduction rule is reflexivity, and the elimination rule is, in essence, the Yoneda Lemma from category theory. When interpreted in terms of homotopy theory, this is the type of *paths *in a space, which is critical for defining the fundamental group(oid) of a space, and to clarifying the hinted-at distinction between weak and strict structure in higher dimensions. More on that later!

By the way, lately Sridhar has been advocating the term “locally V-internal category” as an alternative to “V-enriched category.” It also sounds better without the “V-” prefix.

I’m not sure if it will catch on, but I hope it does.

I think his motivation is to emphasize the fact that every V-internal category is V-enriched, and that enrichment can be seen as a form of internalization without the “global” requirements — namely, no “object of objects” and only a mere monoidal structure rather than all-finite-limits.

Lifting the latter requirement is hugely important for programming languages, where finite limits means equalizers, which means extensional type theory, which means undecidable typechecking. Unfortunately there is [currently] no enrichment-based analogue of Sridhar’s results on Gödel-Löb internal categories… which is really unfortunate for us programmers!

I don’t think it’s really true that every V-internal category is V-enriched, at least not in the generality at which those words are generally used. Internal categories make sense in any category with pullbacks; Enriched categories make sense over any monoidal category. In the special case of a

cartesianmonoidal category which is “lextensive” (i.e. has pullbacks and coproducts behave well), small enriched categories can be identified with “object-discrete” internal categories. But for non-cartesian monoidal structures, or non-extensive categories, neither notion is a special case of the other.Both are, however, special cases of the yet more general notion of a category enriched in a bicategory, or (better) a double category. The phrase “locally internal category” has been used in the past to refer to something equivalent to a locally small fibration, which is also equivalent to a larger version of internal categories (to wit, many-object categories enriched in the bicategory of spans). I’m not sure that I like back-forming it to rename ordinary non-cartesian enriched categories; I think that general bicategory-enrichment is more like classical enrichment than it is like classical internalization.

Ah, just when it seemed like this blog couldn’t get any better, enriched categories come up!

Are you aware of anybody noticing that the context category (contexts are objects, open terms are morphisms — the one you’ve been writing about) of a type theory is enriched in the judgment category (tuples-of-judgments are objects, natural deductions are morphisms from their hypotheses-as-a-tuple to their conclusion) of the same type theory?

Sequents $A\vdash B$ become hom-objects $Hom(A,B)$, and so on. Just about the only requirement is that the cut rule be derivable (not just admissible); this nothing more than the typing rule for “let” in a pure functional language:

$$

{

\Gamma_1 \vdash e_1:\tau_1

\Gamma_2,x:\tau_1 \vdash e_2:\tau_2

\over

\Gamma_1,\Gamma_2 \vdash let x=e_1 in e_2:\tau_2

}

$$

The enrichment relationship above isn’t anything particularly earth-shattering (and in hindsight it’s sort of obvious), but it’s been remarkably hard to figure out who to cite.

I suppose I ought to add that the framework above leads to very concise statements of some of the big ideas in type theory.

For example, the “compositional bijection” part of the LF adequacy theorem amounts to saying that there is a full and faithful monoidal functor from the judgments category (i.e. enriching category) of the theory being formalized to the context category (i.e. enriched category) of $\lambda\Pi$. From this perspective, HOAS works because LF’s context category is cartesian closed.

Moving from cartesian monoidal structure to non-symmetric monoidal structure may yield insight on what an ordered logic analogue of LF ought to look like (IIRC ordered logic was one of the few cases which couldn’t be handled by the technique in Crary’s 2009 paper).

Great post! I do, however, think that the notion of $(\infty,1)$-category is fairly firmly established now. There are many definitions, indeed, but they’re all Quillen equivalent as model categories. (See for instance the nLab page: http://ncatlab.org/nlab/show/(infinity,1)-category)

The same is true for $(\infty,0)$-categories ($\infty$-groupoids), as far as I know.

It is only for $n>1$ that the notion of $(\infty,n)$-category becomes murkier.