Characterizing identity types

In homotopy type theory we often need to characterize the identity type or the loop space of a given type. There is a variety of techniques to do this, but I find myself using one particular technique the most (by far). Occasionally I find myself in a situation where I need to explain this, so I thought I’d also do that here.

It begins by observing that a fiberwise map g:\Pi_{(a:A)}~P(a)\to{}Q(a) is a fiberwise equivalence (i.e. each g(a):P(a)\to{}Q(a) is an equivalence) precisely when it gives an equivalence on total spaces. The map \mathsf{total}(g):(\Sigma_{(a:A)}~P(a))\to{}(\Sigma_{(a:A)}~Q(a)) is defined by


Theorem 1. Let g:\Pi_{(a:A)}~P(a)\to{}Q(a) be a fiberwise map from P:A\to{}U to Q:A\to{}U. Then the following are equivalent:

  1. Each g(a):P(a)\to{}Q(a) is an equivalence,
  2. The map \mathsf{total}(g):(\Sigma_{(a:A)}~P(a))\to{}(\Sigma_{(a:A)}~Q(a)) is an equivalence.

The reason is basically that the fiber \mathsf{fib}_{\mathsf{total}(g)}(a,y) at (a,y):\Sigma_{(a:A)}~Q(a) is equivalent to the fiber \mathsf{fib}_{g(a)}(y). Thus, all the fibers of \mathsf{total}(g) are contractible precisely when all the fibers of each g(a) are contractible.

Now lets focus on characterizing the identity types. Recall that for any type A with a_0:A, the type \Sigma_{(a:A)}~a_0=a is contractible. At the same time, the type of identifications starting at a_0 is the least ‘reflexive type family’ on A. By this, we mean that for any P:A\to{}U with x_0:P(a_0), there is a (unique) fiberwise map g: \Pi_{(a:A)}~(a_0=a)\to{}P(a) which maps \mathsf{refl}(a_0) to x_0. By Theorem 1 above, it follows that this is fiberwise an equivalence precisely when \Sigma_{(a:A)}~P(a) is contractible. Thus, we have:

Theorem 2. Let A be a type with a_0:A, and let P:A\to{}U be a type family with x_0:P(a_0). Then the following are equivalent:

  1. The (unique) fiberwise map g:\Pi_{(a:A)}~(a_0=a)\to{}P(a) that is determined by g(\mathsf{refl}(a_0)):=x_0, is a fiberwise equivalence.
  2. The total space \Sigma_{(a:A)}~P(a) is contractible.

This is how we often prove that a particular, well-chosen type family on a given pointed type A is the identity type. To obtain what is called the encode-decode method, one may further break down the contractibility condition. Nevertheless, Theorem 3 is useful by itself, because in lots of situations there are other means of showing that the total space is contractible. Therefore, this theorem has been for me the most useful tool to in characterizing the identity type of a type.

Also, a slight generalization of Theorem 1 (which I use pretty often) arises when we take a map f:A\to{}B, and a fiberwise map g:\Pi_{(a:A)}P(a)\to{}Q(f(a)), i.e. a fiberwise map g over f. Now we can define \mathsf{total}_f(g):(\Sigma_{(a:A)}~P(a))\to(\Sigma_{(b:B)}~Q(b)) by

\mathsf{total}_f(g,(a,x)) := (f(a),g(a,x)).

Theorem 3. Let f:A\to{}B, and let g:\Pi_{(a:A)}P(a)\to{}Q(f(a)). Then the following are equivalent:

  1. Each g(a):P(a)\to{}Q(f(a)) is an equivalence,
  2. The square
     20161015_1is a pullback square.

One thought on “Characterizing identity types

  1. Pingback: The type of 2-element types | Egbert RIJKE

Leave a Reply

Fill in your details below or click an icon to log in: Logo

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

Google+ photo

You are commenting using your Google+ 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 )

Connecting to %s