One reason why there is no big discussion yet could be that the crisis surfaces only in rigorous type theoretic proof environments such as those provided in the

One reason why there is no big discussion yet could be that the crisis surfaces only in rigorous type theoretic proof environments such as those provided in the proof assistant Coq and others. While Coq has been successfully used to formalize mathematical theorems (a term I use here in contrast to computer science theorem), I am pretty sure few mathematicians use Coq or even type theory in their day to day work. Until that becomes custom, the discussion about HoTT will probably stay in the type theorist community. Interestingly, I also think that only after the crisis is solved we can expect mathematicians to use type theory as foundation for their work.