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 impleme

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.