Source
- URL: https://x.com/LeeeeeeeeeT_/status/2073449105867620454
- Author: LeeeeT (@LeeeeeeeeeT_)
- Posted: 2026-07-04 16:49:24
Branch
1/ @LeeeeeeeeeT_
@VictorTaelin
i once implemented a type checker for impredicative MLTT. i then tried to reproduce hurkens’ paradox (simplified girard’s paradox) - my type checker got stuck in an infinite loop. so.. you couldn’t prove false in it, it just never terminated
Related
- Spine: 2026-07-04-sighs