The distinguishing feature of higher-dimensional type theory is the concept of *equivalence* of the members of a type that must be respected by all families of types. To be sufficiently general it is essential to regard equivalence as a *structure, *rather than a *property. *This is expressed by the judgement

which states that and are equivalent members of type , as evidenced by the transformation . Respect for equivalence is ensured by the rule

which states that equivalent members determine equivalent instances of a family of types. The equivalence between instances is mediated by the operation , which sends members of to members of . We call this mapping the *action *of the family on the transformation .

For reasons that will only become apparent as we go along, it is important that “equivalence” really be an equivalence: it must be, in an appropriate sense, reflexive, symmetric, and transitive. The “appropriate sense” is precisely that we require the existence of transformations

Moreover, these transformations must be respected by the action of any family, in a sense that we shall make clear momentarily. Before doing so, let us observe that these transformations constitute the operations of a *groupoid*, which we may think of either as *an equivalence relation equipped with evidence* or *a category in which every map is invertible (a generalized group)*. While the former interpretation may not suggest it, the latter formulation implies that we should impose some requirements on how these transformations interact, namely the axioms of a groupoid:

- Composition (multiplication) is
*associative*: . - Identity is the
*unit*of composition: and . - Inverses
*cancel*: and .

*equalities*on transformations, demand that the second-dimensional structure of a type form a

*strict groupoid*. I will come back to an important weakening of these requirements later.

We further require that the action of a type family preserve the groupoid structure. For this it is enough to require that it preserve identities and composition:

and

.

Thinking of a groupoid as a category, these conditions state that the action of a type family be *(strictly) **functorial*. (Here again we are imposing strong requirements in order to facilitate the exposition; eventually we will consider a relaxation of these conditions that will admit a richer range of applications.)

(The alert reader will note that I have not formally introduced the concept of a transformation between* types*, nor the equality of these, into the theory. There are different ways to skin this cat; for now, I will be a bit loose about the axiomatics in order to focus attention on the main ideas. Rest assured that everything can be made precise!)

By demanding that the groupoid axioms hold strictly (as equalities) and that the action of families be strictly functorial, we have simplified the theory considerably by restricting it to dimension 2. To relax these restrictions requires higher dimensions. For example, we may demand only that the groupoid conditions hold *up to a transformation of transformations*, but hold strictly from then on; this is the 3-dimensional case. Or we can relax all such conditions to hold only up to a higher transformation, resulting in *finite dimensional type theory*. Similar considerations will apply to other conditions that we shall impose on the action of families, in particular to specify the action of type constructors on transformations, which I will discuss next time. The presentation of finite-dimensional type theory will be aided by the introduction of *identity types* (also called *path types*). Identity types avoid the need for an ever-expanding nesting of transformations between transformations between …. More on that later!

*Update (August 2012)*: Egbert Rijke has written lucidly on the topic of Yoneda’s Lemma and it’s relation to homotopy type theory in his Master’s Thesis, which I encourage readers to consult for a nice summary of higher-dimensional type theory.

Has anyone thought about whether there are any natural categorifications of the notion of

partialequivalence relations? (It’s not obvious to me how to do this, since PERs are not necessarily reflexive.) Still, it would be really great if there were some version of System F + dependent types, in which propositional equality was parametric.“Or we can relax all such conditions to hold only up to a higher transformation, resulting in ‘finite dimensional type theory’.”

I suppose I must just be misinterpreting this in some way, but if all coherence conditions at all levels are only up to a coherence isomorphism at the next deeper level, why would this not be

infinite-dimensional type theory (infinite in the sense of corresponding to infinity-groupoids)?It would, I had a terminological slipup.

Since we Germans prefer everything in sausage form, including words, it is actually Jawohl!

(Surprisingly, though, Herrdreyer is not something anybody would ever write, not even in Saarbrücken.)

Ja wohl!

Your cancel rule says “a” where it should say “id”. Also, you have a stray \emph in the last paragraph.