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 is a fiberwise equivalence (i.e. each is an equivalence) precisely when it gives an equivalence on total spaces. The map is defined by

.

**Theorem 1.** *Let be a fiberwise map from to . Then the following are equivalent:*

*Each is an equivalence,*
*The map is an equivalence.*

The reason is basically that the fiber at is equivalent to the fiber . Thus, all the fibers of are contractible precisely when all the fibers of each are contractible.

Now lets focus on characterizing the identity types. Recall that for any type with , the type is contractible. At the same time, the type of identifications starting at is the least ‘reflexive type family’ on . By this, we mean that for any with , there is a (unique) fiberwise map which maps to . By Theorem 1 above, it follows that this is fiberwise an equivalence precisely when is contractible. Thus, we have:

**Theorem 2.** *Let be a type with , and let be a type family with . Then the following are equivalent:*

*The (unique) fiberwise map that is determined by , is a fiberwise equivalence.*
*The total space is contractible.*

This is how we often prove that a particular, well-chosen type family on a given pointed type 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 , and a fiberwise map , i.e. a fiberwise map over . Now we can define by

.

**Theorem 3.** *Let , and let . Then the following are equivalent:*

*Each is an equivalence,*
*The square*

* is a pullback square.*

### Like this:

Like Loading...

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