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 .
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:
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.