Timeline for General method for disproving possibility of judgemental equality
Current License: CC BY-SA 4.0
6 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Aug 11, 2023 at 2:52 | answer | added | cody | timeline score: 3 | |
| Aug 10, 2023 at 15:58 | comment | added | Trebor♦ | @cody Ah, nice argument. I think that's already worth an answer (perhaps with some generalizations). | |
| Aug 10, 2023 at 15:49 | comment | added | cody | Because any normal form of the LHS would have to be $\alpha$ equivalent to itself, with the variables $x$ and $y$ swapped (since reduction in MLTT commutes with substitution). It's not too hard to see that such a term cannot exist. | |
| Aug 10, 2023 at 3:45 | comment | added | Trebor♦ | @cody Can you elaborate on the termination argument? Why can't they both reduce to a common expression? | |
| Aug 9, 2023 at 18:23 | comment | added | cody | If you have $x + y = y + x$ judgmentally with $x$ and $y$ variables, this easily contradicts termination of MLTT computation. Without that you'll need a more subtle argument. Note that the free monoid over a finite decidable type can be encoded using a clever NbE trick. | |
| Aug 8, 2023 at 14:34 | history | asked | Trebor♦ | CC BY-SA 4.0 |