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.
Revision on May 1, 2022 at 20:15:57 by Anonymous?. See the history of this page for a list of all contributions to it.