The *identity inductive type family* is one of the most subtle parts of Type Theory, and is core of the link to topology. Here we clarify the definition and some basic properties. Note that there is no additional rule required for this - instead its rich structure depends on the power of induction for indexed types.

Fix a type $A$. We define $Id_A : A \to A \to \mathcal{U}$ as follows:

**Definition:** $Id_A : A \to A \to \mathcal{U}$ is the *indexed inductive type family* freely generated by

- $refl_A : \prod_{a : A} Id_A (a)(a)$

We also denote $Id_A(p)(q)$ as $p =_A q$ or simply $p = q.

Fix a type $A$. Informally, the induction principle for the indexed identity type family says that to define a dependent function $f$ on all elements of the family $Id_A$, i.e. triples $(p : A, q : A, \alpha: p =_A q)$ it suffices to define $f$ on triples where $p=q$ and $\alpha= refl_A (p)$.

Formally, a type family $Q$ on $Id_A$ is a term $Q : \prod_{p, q: A} Id_A(p)(q) \to \mathcal{U}$, i.e. for $p, q: A$ and $\alpha : p =_A q$ we get a type $Q(p)(q)(\alpha)$. The induction principle (which is an instance of the general rule for indexed types) says that given such a family $Q$, we can introduce a term

Furthermore, if $\varphi: \prod_{p: A} Q(p)(p)(refl_A(p))$ (i.e., $\varphi$ is the data for the inductive definition) and $p_0: A$, then

We typically use the induction function by giving as *input* a term in the domain, which corresponds to $p=q$ and $\alpha= refl_A (p)$.

Our first application illustrating this is to show symmetry of equality. Symmetry corresponds to the type

which we can also write as

The second form corresponds to the type family $Q = (p: A) \mapsto (q: A) \mapsto (\alpha: p =_A q) \mapsto q =_A p$, i.e. we have

Hence, we just have to give as argument a term in the domain of this function. Indeed, we can define

and see that $\sigma_A : \mathcal{S}_A$. Thus we have a term that proves symmetry.

We also observe that the identity $\sigma_A(p)(refl_A(p))\equiv refl_A(p)$.

**Topology:** The operation $\sigma_A$ is reversing the direction of a path. The identity says that reversing a constant path gives itself.

To make our life easier, we formulate a type corresponding to *transitivity* in a slightly unnatural form. It is an exercise to construct a function from this to a more natural form - such a function is a proof that our formulation implies the natural one.

Namely, we define the type

This corresponds to the type family

in the sense that (as $Q_1(p)(p)(refl_A(p)) = \prod_{r: A} \prod_{\beta : p =_A r} p =_A r$) $\mathcal{T}_A$ is the codomain of the induction function

To construct an element of $\mathcal{T}_A$, we need to construct an element of the domain $D = \prod_{p: A} \prod_{r: A} \prod_{\beta : p =_A r} p =_A r$ of $ind_{Id_A, Q_1}$. We do this by applying induction again, this time for the type family $Q_2 := (p: A) \mapsto (r : A) \mapsto (\beta: p =_A r) \mapsto p =_A r$. We see that

and relexivity in the domain of this induction function. Thus, we can define

so that $\tau_A : \mathcal{T}_A$. Thus we have proved transitivity.

**Identities:** Since we used induction twice, it takes two steps to unravel the idenities that $\tau_A$ satisfies. Firstly, the induction with respect to $Q_1$ gives the identities

By itself this is not very useful. However we apply the identity for induction with respect to $Q_2$ to get

This says that transitivity of two equalities by reflexivity (for a term $p: A$) is equality by reflexivity.

**Topology:** The operation $\tau_A$ is joining two paths when the terminal point of the first coincides with the initial point of the second. The identity says that joining two constant paths at the same point $p : A$ gives the constant path at $p$.