Well, I will defer to your judgment! I’m by no means a type theory person.

My understanding was that these features are how quotients are managed to be implemented. But perhaps that is wrong.