[math-fun] HoTT foundations of maths

Well, I wish somebody had a bit to say about applications or motivations. I mean, was there something broke that needed to be fixed? Can it do stuff you could not do before, clears up issues, what? Is the point that it meshes better with attempts to build automated theorem provers? It sounds vaguely reasonable.