Transformations as strict groupoids


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

\displaystyle \Gamma\vdash \alpha::M\simeq N:A

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

\displaystyle{{\Gamma,x:A\vdash B\,\textsf{type}\quad  \Gamma\vdash \alpha :: M\simeq N:A \quad  \Gamma\vdash P:B[M/x]}\over  {\Gamma\vdash \textit{map}\{x:A.B\}[\alpha](P):B[N/x]}},

which states that equivalent members determine equivalent instances of a family of types.  The equivalence between instances is mediated by the operation \textit{map}\{x:A.B\}[\alpha](-), which sends members of B[M/x] to members of B[N/x].  We call this mapping the action of the family x:A.B on the transformation \alpha.

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

\displaystyle{\Gamma\vdash \textit{id}::M\simeq M:A}

\displaystyle{{\Gamma\vdash\alpha::M\simeq N:A}\over{\Gamma\vdash\alpha^{-1}::N\simeq M:A}}

\displaystyle{{\Gamma\vdash \beta:N\simeq P:A\quad  \Gamma\vdash \alpha:M\simeq N:A}\over{\Gamma\vdash\beta\circ\alpha:M\simeq P:A}}

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:

  1. Composition (multiplication) is associative: \gamma\circ(\beta\circ\alpha)\equiv (\gamma\circ\beta)\circ\alpha::M\simeq N:A.
  2. Identity is the unit of composition: \textit{id}\circ\alpha\equiv\alpha::M\simeq N:A and \alpha\circ\textit{id}\equiv\alpha::M\simeq N:A.
  3. Inverses cancel: \alpha^{-1}\circ\alpha\equiv\textit{id}::M\simeq M:A and \alpha\circ\alpha^{-1}\equiv\textit{id}::N\simeq N:A.
These conditions, which impose 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:

\displaystyle{\textit{map}\{x:A.B\}[\textit{id}](-) \equiv \textit{id}(-):B[M/x]}

and

\displaystyle{\begin{array}{c}\textit{map}\{x:A.B\}[\beta\circ\alpha](-)\\\equiv\\\textit{map}\{x:A.B\}[\beta](\textit{map}\{x:A.B\}[\alpha](-))\end{array}}.

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.

About these ads

6 Responses to Transformations as strict groupoids

  1. neelk says:

    Has anyone thought about whether there are any natural categorifications of the notion of partial equivalence 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.

  2. Sridhar Ramesh says:

    “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)?

  3. 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.)

  4. Abstract Type says:

    Ja wohl!

  5. herrdreyer says:

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

Leave a Reply

Please log in using one of these methods to post your comment:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

Follow

Get every new post delivered to your Inbox.

Join 1,014 other followers

%d bloggers like this: