Showing changes from revision #3 to #4:
Added | Removed | Changed
A homotopy type theory is a dependent type theory where every type is a homotopy type, or equivalently where every type has some sort of identity type between any two terms of the type.