模板: 类型论

根据香蕉空间的设计目标, 类型论板块尽可能只关注现代类型论, Russell 那一套东西、计算机相关 (比如面向对象类型系统) 就不要划在类型论板块里了.

板块完善计划：

重构Martin-Löf 类型论词条，将关于变量的部分转化为非正式的处理，并且将形式化处理变量的部分转移到单独的词条。我计划介绍两种实现：DBI (De Bruijn 编号)、LN (仅局部无名), 可以简单介绍下 LNS (局部无名集). 不介绍 CAS.
概括范畴内容太少, 可以写的更具体的. 需要一个读过 Bart Jacobs 的人去写.
立方类型论可以直接搬运 https://ice1000.org/typst-workbench/cubicalmethods.pdf , 只是我一直没时间去做. 感兴趣的人可以找我要文章的源码, 但这个是 typst 写的.
参数性中的内化一节 (internal parametricity). 目前我并不认识掌握这方面知识、又会中文的人. 可能是未来的我自己.
Tait 可计算性现在还没有, 以及需要简要介绍综合 Tait 可计算性.
具现内容非常匮乏. 可以考虑和有效意象联系起来.
归纳类型相关内容非常不完善. 需要解释严格正性和给 theory of signatures 想一个更好的翻译, 目前想的是下面的语汇理论, 我觉得这个翻译不太好, 但我也非常不想叫它 "签名".
纯类型论没写, 但这个对别的词条比较重要, 比如F 系统肯定和它有联动.