# 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

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

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
is a pullback square.