#
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