[chriswarbo]

I haven't used quotients (or Lean), but I've certainly encountered subject reduction problems in Coq when using coinduction, so this sounds a tad hypocritical.

It's certainly good to avoid breaking subject reduction even more though ;)

[Jweb_Guru]

Pierre Pedrot has been very vocal in his belief that broken SR from coinductive types is a serious problem with Coq that needs to be fixed. This is quite different from introducing stuff that deliberately breaks it.

[xvilka]

There's ongoing work[1] on fixing that. Also let's see how migrating setoids to cubical type theory might fix more issues for Coq. Will they follow the Arend[2] path? That remains to be seen.

[1] https://github.com/coq/coq/pull/10764

[2] https://arend-lang.github.io/about/arend-features