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

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

Definition

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