Showing changes from revision #0 to #1:
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.