It's an open secret that while HoTT has the clear potential to be relevant for practicing homotopy theorists and higher topos theorists, the field is not yet quite living up to it. There are a tiny number of people, first and foremost Mike Shulman, who really work on HoTT as a topic in higher topos theory. The progress especially Mike has been making is impressive, but to homotopy theorists who are not into type theory or foundations as such, the development of HoTT is still at most at the verge of being interesting.

Lurie's often quoted "no comment", as in this recent hott-cafe discussion:

https://groups.google.com/d/msg/hott-cafe/oBRMrk17G0I/C9SBjrPaAQAJis just the most prominent example, I could give you a long list of names of top homotopy theory researchers who ought to be interested in HoTT-as-it-could-once-be but are dismissive about it at the moment.

I think this ought to change, and it may change. But changing this situation will require more man-years of work on the aspects of HoTT that are genuinely homotopy theoretic and higher topos theoretic.

Unfortunately, currently large parts of the field are actively pushing away from this direction, wich does not help to improve the situation.

For instance all the work on initiality of models of type theory is really something that belongs to traditional type theory and means nothing to practicing mathematicians. One sees vivd evidence this week where at MPI Bonn Vladimir is giving a "marathon", as he announced it, talk series on C-systems in the context of a program titled "Higher structures in geometry and physics": it leaves most people except a handful of accounting specialists utterly puzzled why they should care about this, and nobody gets away with the impresion that there is anything to be gained here for researchers in "higher homotopy structures".

Also the wealth of work on "cubical type theory" so far failed to really connect to homotopy theory as such. The problem that it is motivated by, to make univalence compute, is again something that research homotopy theorists could not care less about; it's pushing away from instead of towards the interest of homotopy theorists.

In contrast, I think it is clear that what needs to be done next in order to improve the impact of HoTT on research-level homotopy theory is:

First and foremost, fill that darn remaining issue with the weak Tarskian universes, such as to finally have as an official theorem (instead of as something that Mike Shulman finds too obvious to publish, while nobody else in the field understands) that HoTT has interpretation in

**every** infinity-topos as in Lurie's book, not just in the (admittedly already impressive) two or three classes of infinite families of infinity-presheaf toposes (with strict universes) that Mike has, thankfully, constructed. Mike explained this here

https://ncatlab.org/homotopytypetheory/show/model+of+type+theory+in+an+(infinity,1)-toposand if I were in charge of HoTT, I would drop everything else until the statement on that webpage becomes an officially published article.

Second, really important would be to make progress on formalizing stable homotopy theory, i.e. "spectrum types" or at least something in this direction. Homotopy theory is so rich, that most computational progress in practice is made by "linearizing" problems, in the sense of Goodwillie calculus, hence by translating problems about homotopy types into problems about stable homotopy types (spectra) as far as possible.

For instance it's not too surprising that the HoTT community is currently stuck with computing but the most evident homotopy groups of spheres (another reason why any working homotopy theorist feels there is nothing to be found here): this was precisely the state of the field of homotopy theory, too, in the 50s, before stabilization and spectral sequences came along.

Again, it's Mike Shulman who has started to push this topic from a HoTT perspective

https://ncatlab.org/homotopytypetheory/show/spectral+sequencesbut it would be useful if more people in the field (anyone, for that matter) picked this up and developed this further.

Spectral sequences is

**the** tool in modern research level homotopy theory (see the recent sensational proof of the Kervaire invariant one problem), it's where all the meat it. But also, it's computationally demanding. Therefore, potentially, there is a fantastic chance here for any computer assisted homotopy theory, hence for HoTT. Once you had a piece of Coq that would read in a tower of homotopy types and which would then start crunching out the pages of its spectral sequence, you would be assured that all those homotopy theorists who previously had "no comment" to make on HoTT would start paying attention.

In short, I think currently HoTT as a topic in homotopy theory has an large ratio of potential over realization. Anybody who cares should think about investing more energy into research that actually goes in this direction. Go and contact Mike Shulman, if you are not sure which precise research questions to tackle. Read all his articles, to see what the state of the field of HoTT as a topic in homotopy theory is. Then work on this. I am optimistic that with effort spend in this direction, eventually homotopy theorists who had not been interested in type theory as such will take notice.