Homotopy Type Theory identity type > history (Rev #3, changes)

Showing changes from revision #2 to #3: Added | Removed | Changed

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 higher inductive type

References

HoTT book