Homotopy Type Theory homotopy type theory > history (Rev #5, changes)

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

Examples

• Martin-Loef type theory
  • book homotopy type theory
• cubical type theory?
• higher observational type theory

See also

• dependent type theory
• univalent type theory

References

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