Homotopy Type Theory homotopy type theory > history (Rev #2)

Definition

Homotopy type theory is a dependent type theory where every type is a homotopy type, or equivalently where every type has an identity type between any two terms of the type.

See also

• dependent type theory
• univalent type theory
• intensional Martin-Loef type theory
• cubical type theory?
• higher observational type theory

References

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