Mike Shulman

Surely in the presence of arbitrary rewrites (especially non-confluent ones), definitional equality was already no longer transitive (at least, not in a way verifiable by the conversion checker)?

Is there any prospect of fixing this issue? Even if the underlying problem #4272 is too much work to fix, could some band-aid be implemented for rewrite rules specifically? This...

I got a similar error elsewhere in my code: ``` de Bruijn index out of scope: 9 in context [x, x, x, x, x, x] CallStack (from HasCallStack): error, called...

Would it be helpful in fixing this if I were able to make the test case smaller? (Sorry if this is a dumb question, I don't really have any idea...

Fantastic! Thanks for fixing this, even with such a long test case. As I expected, the fix has also fixed the other similar error.

I'm using Emacs and I just tried out the sample linked to in the report and see the same behavior with Agda 2.5.1.1. Commenting out the imports and replacing them...

I think the relevant thing to determine whether a given elimination into non-fibrant types is valid should be whether the *inductive definition* that's being eliminated is one that was declared...

By the way, I have a concrete reason to need to combine `--two-level` with `--cumulativity`, not just for convenience. As Elif said, this combination allows defining a single strict equality...

(Also by the way, this isn't related to cumulativity, but it appears to be still possible to define a map `⊥ → ⊥ᵉ` from the fibrant empty type to the...

Regarding the question of consistency: if you can eliminate the fibrant equality type into the non-fibrant one, then you can prove that they're equivalent and hence both satisfy UIP; so...