I have been trying for some time to understand what Homotopy Type Theory or Univalent Foundations is actually about. The HOTT book announces a new branch of ma

I have been trying for some time to understand what Homotopy Type Theory or Univalent Foundations is actually about. The HOTT book announces a new branch of mathematics, what is it? Martín Escardó addresses this directly at the beginning with his 8 points. HOTT is a Martin-Löf Type Theory variant. MLTT has been developing since at least 1970, so it's not exactly brand new. In contrast to First Order Logic and Zermelo Fränkel Set Theory, MLTT works with types that are constructed and applied according to certain rules. Some of the rules are more logical (Cartesian product = conjunction, function = implication) some are more mathematical (induction rules, e.g. for natural numbers). Martin-Löf's innovations are the Dependent Types (corresponding to logical quantifiers) and the Identity Types. Identity types have always been somewhat mysterious; equality actually seems to be the simplest thing in the world. On the one hand, two expressions are equal if they have the same simplification (assuming confluence). This is called definitional (extensional) equality. But there is also equality that has to be proven (differently), that is intensional equality. Definitional equality implies intensional equality (the expressions are equal => their equality is proven). HOTT now sees a non-trivial structure in the proofs of equality. Various equality proofs are possible. One level higher, however, there is the possibility of proving the equality of equality proof and on and on. This is an infinity groupoid or homotopy type. This results in a hierarchy of mathematical objects. At the bottom are objects whose equality is trivial (old school sets and propositions). The new ones are the Higher Types, whose elements (e.g. cell complexes) are complicated set constructions in traditional mathematics. For Univalence I better refer to Point 3, otherwise I would write that Univalence enables treating equal Objects as equal.