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 iso

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)