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

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

Definition

In dependent type theory, a homotopy type is a type with some sort ofidentity 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)