Quotients are a bit of an unsolved problem even in Agda. Cubical Agda makes the definition easier but makes it much harder to work with the resulting datatype,

Quotients are a bit of an unsolved problem even in Agda. Cubical Agda makes the definition easier but makes it much harder to work with the resulting datatype, while if you don't use higher inductive types you end up in setoid hell where the language can't do any of the obvious things you should be able to do automatically.