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
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$.