Homotopy Type Theory identity system > history (Rev #2, changes)

In homotopy type theory, an identity system on a type $A$ is a dependent type $a:A \vdash R(a,a)$ indexed by the product type $A \times A$ with a dependent function

such that for any dependent type

and dependent function

there exists a dependent function

and a dependent function

See also

• dependent type theory
• identity type
• homotopy type
• homotopy type theory

References

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