HoTT isn't a programming language, because there are non-value normal forms. That's the whole reason behind research into various formulations of Cubical Type Theory, which is a programming language.
Intensional intuitionistic type theory is a programming language. Throw in higher inductive types (still a programming language at this point) and Voevodsky's univalence and you've got HoTT. Then sure, the simplicial model is not constructive, whereas the cubical models give computational meaning to univalence, but they're still just that, models of HoTT. So would you prefer I had said HoTT has models that are programming languages?
analbumcover|5 years ago