Not the OP, but the cool thing about HoTT to a user of proof assistants is that it makes working with "quotients" easier. I put quotients in parentheses because

Not the OP, but the cool thing about HoTT to a user of proof assistants is that it makes working with "quotients" easier. I put quotients in parentheses because really HoTT is about generalizing the idea of a quotient type. Quotients of sets/algebras are one of the core tools of mathematics and old school type theory doesn't have them so you have to manually keep around equivalence relations and prove over and over again that you respect the relations. In HoTT, there is an extension of inductive types that allows you to, not just have constructors, but also to impose "equalities" so these generalized "quotients" really have first-class status in the language. As far as "exciting developments" in HoTT, the big one right now is Cubical Type Theory [1], which is the first implementation of the new ideas of HoTT where Higher inductive types and the univalence axiom "compute" which means that the proof assistant can do more work for you when you use those features. I just saw a talk about it and from talking to people about it, this means that it won't be too long (< 5 years I predict) before we have this stuff implemented in Agda and/or Coq. Finally, I just want to say to people that are scared off or annoyed by all of the abstract talk about "homotopies" and "cubes", you have to understand that this is very new research and we don't yet know the best ways to use and explain these concepts. I certainly think that people will be able to use this stuff without having to learn anything about homotopy theory, though the intuition will probably help. [1] https://github.com/mortberg/cubicaltt https://github.com/mortberg/cubicaltt