Interesting, do you think these ideas will have applications in CS ?
I mean type theory is obviously useful, both to things like formal proofs and the definition of typed languages but do you think that thinking of types in terms of topological spaces and homotopy will lead to new insights in these or related areas ?
It depends how you define CS; some people I work with don't consider CS and Maths to be different subjects ;)
Personally, I find the topological perspective useful for thinking about types. I would guess most programmers think of types as sets, which is perfectly fine for the kind of first-order tasks we encounter in almost all day-to-day programming. However, it doesn't give much intuition when dealing with the crazy kinds of abstractions we find in languages like Coq, Agda, or even some of the funky new Haskell extensions. Whilst the vast majority of programmers will never, and should never need to, deal with that level of abstraction, it's personally the kind of programming I really enjoy :) (My own work is in the area of formal proofs, proof search, program equivalence, etc.)
I think HoTT's key insight has already been made: although using UIP (or one of its many equivalents) to ignore the differences between proofs makes life easier in the short-term (eg. as a Coq user I was blown away by Agda's ability to do pretty much everything by pattern-matching on refl), in the longer term all of those transport lemmas, path inductive proofs, etc. give us tangible benefits; firstly for explaining why something is true, secondly for allowing new kinds of higher-level reasoning and thirdly for aiding mechanisation and computation. Essentially, HoTT is just a logical extension of the intuitionism/constructivism ideals :)
Hopefully HoTT, or something very much like it, will narrow the gap between what people know and what machines know.
"Hopefully HoTT, or something very much like it, will narrow the gap between what people know and what machines know."
Yeah I was actually thinking along the same lines.
There seems to currently be a major disconnect in abstraction ability between humans and any AI approach I'm aware of. Humans seem to have an apparently unlimited ability to move between levels of abstraction while algorithms seem tied to the specific abstractions used in designing them. Or in other words it seems like AI algorithms are always stuck in some particular box while humans can always expand their box, or even jump to another one entirely.
Unfortunately my knowledge of these fields (type theory, algebraic topology, etc.) is so limited that I have no real idea of how HoTT could help with this, beyond the vague notion that it might.
I mean type theory is obviously useful, both to things like formal proofs and the definition of typed languages but do you think that thinking of types in terms of topological spaces and homotopy will lead to new insights in these or related areas ?