https://abooij.github.io/wiwikwlhott/
- univalence axiom
- higher inductive types
"Both ideas are impossible to capture directly in classical set-theoretic foundations, but when combined in homotopy type theory, they permit an entirely new kind of "logic of homotopy types"." p13
invariance, homotopy
univalence foundations
Russell -> Church -> Martin-Löf
• Types added to objects can be used to reason upon it.
"an object of function type A -> B can be acquired from an object of type B parametrized by objects of type A, and can be evaluated at an argument of type A." p14
• function as parametrization or dependency
extensive use computer proof assistants
"We believe that the new idea of regarding types, not as strange sets (perhaps constructed without using classical logic), but as spaces, viewed from the perspective of homotopy theory, is a significant step forward. In particular, it solves the problem of understanding how the notion of equality of elements of a type differs from that of elements of a set." p14
"A homotopy between a pair of continuous maps f: X -> Y and g: X -> Y is a continuous map H: X * [0, 1] -> Y satisfying H(x, 0) = f and H(x, 1) = g(x). The homotopy H may be thought of as a "continuous deformation" of f into g. The spaces X and Y are said to be homotopy equivalent, X ~ Y, if there are continuous maps going back and forth, the composites of which are homotopical to the respective identity mappings, i.e., if they are isomorphic "up to homotopy". Homotopy equivalent spaces have the same algebraic invariants (e.g., homology, or the fundamental group), and are said to have the same homotopy type." p14
a: A term a is of type A a is a point of the space A
"spaces are treated purely homotopically, not toplologically." p15
∞-groupoids name for the "invariant objects"
"(It is tempting to also use the phrase homotopy type for these objects, suggesting the dual interpretation of “a type (as in type theory) viewed homotopically” and “a space considered from the point of view of homotopy theory”. The latter is a bit different from the classical meaning of “homotopy type” as an equivalence class of spaces modulo homotopy equivalence, although it does preserve the meaning of phrases such as “these two spaces have the same homotopy type”.)" p15
"The key new idea of the homotopy interpretation is that the logical notion of identity a = b of two objects a, b: A of the same type A can be understood as the existence of a path p: a ~> b from point a to point b in the space A. This also means that two functions f, g: A -> B can be identified if they are homotopic, since a homotopy is just a (continuous) family of paths p_x: f (x) ~> g(x) in B, one for each x: A. In type theory, for every type A there is a (formerly somewhat mysterious) type Id_A of identifications of two objects of A; in homotopy type theory, this is just the path space A^I of all continuous maps I -> A from the unit interval. In this way, a term p: Id_A(a, b) represents a path p: a ~> b in A." p15
• equation of A type, X == Y: A and A should come with implementation of "==" like "type A: ...". x, y: A ト Id_A(x, y)