3 ms·
The normalization issue is not about quotients at all. It's https://arxiv.org/abs/1911.08174 https://arxiv.org/abs/1911.08174 "Failure of Normalization in Impre
by SkySkimmer 7y ago
The normalization issue is not about quotients at all. It's https://arxiv.org/abs/1911.08174 https://arxiv.org/abs/1911.08174 "Failure of Normalization in Impredicative Type Theory with Proof-Irrelevant Propositional Equality"
- jmgrosen 7y agoWell, 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.