# Homotopy Type Theory identity type

## Idea

The identity type has elements that are witnesses to the “sameness” of elements.

## Definition

### In Martin-Loef type theory

The identity type $=_A : A \to A \to \mathcal{U}$ can be defined as the inductive type? with the following constructor:

• for any $a:A$, an element $refl_A: a=_A a$

### In higher observational type theory

Identity types have the following formation rule

$\frac{A:\mathcal{U} \quad a:\mathcal{T}_\mathcal{U}(A) \quad b:\mathcal{T}_\mathcal{U}(A)}{\mathrm{id}_A(a, b):\mathcal{U}}$