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

Showing changes from revision #8 to #9: Added | Removed | Changed

Idea

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

Definition

In Martin-Loef type theory

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$

In cubical type theory

In higher observational type theory

Identity types have the following formation rule

See also

• dependent type theory
• dependent identity type?
• homotopy type
• identity system
• homotopy type theory
• higher inductive type
• transport

References

• Univalent Foundations Project, Homotopy Type Theory – Univalent Foundations of Mathematics (2013)

• Mike Shulman, Towards a Third-Generation HOTT Part 1 (slides, video)