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

In dependent type theory, a homotopy type is a type with some sort of identity types between any two terms in the type.

See also

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

References

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