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:

  • for any a:Aa:A, an element refl A:a= Aarefl_A: a=_A a

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

Last revised on April 30, 2022 at 20:03:20. See the history of this page for a list of all contributions to it.