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