Post #2775970
2026-05-12 19:03 UTC
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.
Replies (2)
-
@jeanas@mathstodon.xyz 2026-05-12 19:52
@totbwf@types.pl @ncf@types.pl By the way, how technically feasible would it be to make Mikan translate pattern matching and recursion to eliminators?
-
@jesper@agda.club 2026-05-13 13:03
@totbwf@types.pl Thanks, I've created an issue for it at github.com/agda/agda/issues/8564