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!