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

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

Definition

Homotopy type theoryA is a homotopy type theory is a dependent type theory where every type is a homotopy type, or equivalently where every type has an some sort ofidentity 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)