Post #2461472
2026-05-12 18:50 UTC
Another day another proof of false...
Replies (1)
-
@totbwf@types.pl 2026-05-12 19:03
https://gist.github.com/TOTBWF/b3dbe1fb1b62018fe40870163a72e532 Basic problem is that positivity checking mutual definitions can be tricked by (a) preventing it from seeing the entirety of a Pi type and (b) adding a layer of indirection Credit to @ncf@types.pl for the idea that things like `(tt : ⊤) → ⊤-rec tt (Set → Set)` could fool the positivity checker.