Brazilian type checking http://math.andrej.com/2014/05/06/brazilian-type-checking/ : おお。面白そう。
(equality reflection rule を持つような)外延的型理論はシンプルな一方で型検査が決定不能で、それに対して内包的型理論では型検査は決定可能だけれど色々と官僚的で面倒くさい。AgdaとかCoqは内包的型理論。
で、ここで提案しているBrazilはその両方の等号を持つ型理論で、型検査の非決定性については、型検査が停止した時には正しい結果になっていれば良いという割り切りと、型検査のためのヒントを、証明項の比較の際には無視される形で記述可能にすることで対応している。
ただ、このネーミングはどうなんだ……
あと、外延的な型理論にもとづいているはずのNuprI辺りのアプローチと比べるとどうなんだろう？