Showing changes from revision #1 to #2:
Added | Removed | Changed
Homotopy type theory is a dependent type theory where every type is a homotopy type, or equivalently where every type has an identity type between any two terms of the type.