HoTT is very interesting to people working on programming language theory. I, for one, expect we will see a handful of very interesting research programming lan

HoTT is very interesting to people working on programming language theory. I, for one, expect we will see a handful of very interesting research programming languages coming out in the near-future with HoTT-based features, which will allow a lot of stuff which is currently inefficient to do in functional languages to be implemented in very efficient (and provably safe) ways. Sure, that's very much a niche and we can't be sure anything practical will come out of it, but for some of us it's interesting in its own right. :) I understand how this isn't interesting to folks working on pure math, just as category theory likely isn't, but it's the fact that these mathematical abstractions map so well onto (certain kinds of) programming that makes them such recurrent topics on HN.