Comment by zozbot234

I'd also like to know more about that. My comment points out some things about HoTT that might be described as "downsides" by some but are more like things that people might expect from HoTT given that it 'handles' type equality in a rigorous yet flexible way, but aren't actually feasible in a rigorous treatment, i.e. the system is not going to pick up all the issues that are "brushed aside" in an informal treatment and resolve them on its own. Its behavior will point out to you that these issues exist, but you'll still have to do a lot of work dotting the i's and crossing the t's, as with any formalization.