[epilys]

HoTT is certainly esoteric and impenetrable for outsiders. It could even be a bunch of gibberish technobabble and we couldn't tell the difference because there's no effort to reach outside their target group and that's quite small. People seem to praise it so perhaps some day I will be able to enjoy it as well.

[R0b0t1]

It is and is not really relevant for non-mathematicians. If there is finally an digitization of the system then I suspect programmers will find it useful, but until then, it is useful for exploring mathematics separate from set theory. E.g. instead of picking one or the other for a set theory axiom, choose neither.

Probably applicable to finding complexity proofs as well, and optimization.

I reached, some time ago, the conclusion that you could compare programs for equality and determine if they are equal. This traversal of the graph/type theory representation of the program can be NP hard, but it may also not be, and could save lots of time in fields like automatic differentiation by pruning possible solutions that don't need to be evaluated.

To some surprise I'd found other people mentioning this as well.