I keep trying to get the gist of type theory and it's like eating unflavored jello.
E.g. it’s hard for me to imagine how homotopy, which is about continuous deformations of continuous functions, could give leverage in ToC, where nothing is continuous. Presumably I’m missing something because I haven’t even bothered to look this up, but
-
-
To make an analogy: Euclid's Axioms :: Real Cartesian Plane as Homotopy Type Theory :: Spaces of various sorts. We work up to homotopy equivalence, so all the data you care about can be presented combinatorially...
-
e.g. the HoTT "circle" is freely generated by a point and a primitive-axiomatic path between that point and itself. This _means_, e.g. that to map it somewhere else is to give a loop there.
- 8 more replies
New conversation -
-
-
There are pre-existent models of homotopy types that are completely discrete (e.g. Kan complexes). The idea is that a homotopy type is something more fundamental than "just" a byproduct of taking topological spaces modulo a specific equivalence relation.
Thanks. Twitter will use this to make your timeline better. UndoUndo
-
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.