typing-vs-typechecking 里面说 Nuprl 是直觉类型论

[ice1000]

实际上它是一个演化版本叫 computational type theory。 Martin-Löf 直觉类型论是没有 Nuprl 里面那些 quotient、equality reflection 之类的东西的。你看怎么翻译比较好吧 ：)