[SkySkimmer]

The normalization issue is not about quotients at all. It's https://arxiv.org/abs/1911.08174 "Failure of Normalization in Impredicative Type Theory with Proof-Irrelevant Propositional Equality"

[jmgrosen]

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.