[m_j_g]

From my experience ability to turn equivalences to equlities and vice versa is very usefull. Without this you are ending in setoid hell - intracable mess of isomorphism. I suspect that also Higher Inductive Types have lots of potential to simplify practical verification effords (apart from obvious usecases of quotients and truncations)

[orangea]

It is my understanding that HITs are just as easy to integrate into non-homotopy type theories as they are to HoTTs.