### Identity Type Family

#### Date: 08 March 2019

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.

## The definition

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