Homotopy Type Theory
identity type


The identity type has elements that are witnesses to the β€œsameness” of elements.


In Martin-Loef type theory

The identity type = A:Aβ†’A→𝒰=_A : A \to A \to \mathcal{U} can be defined as the inductive type? with the following constructor:

In cubical type theory

In higher observational type theory

Identity types have the following formation rule

A:𝒰a:𝒯 𝒰(A)b:𝒯 𝒰(A)id A(a,b):𝒰\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}}

See also


category: type theory