# Homotopy Type Theory identity type

## Idea

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

## Definition

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$

## See also

higher inductive type

## References

HoTT book

category: type theory

Last revised on October 11, 2018 at 08:59:46. See the history of this page for a list of all contributions to it.