模板: 类型论

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

板块完善计划：

• 重构Martin-Löf 类型论词条，将关于变量的部分转化为非正式的处理，并且将形式化处理变量的部分转移到单独的词条。我计划介绍两种实现：DBI (De Bruijn 编号)、LN (仅局部无名)，可以简单介绍下 LNS (局部无名集)。不介绍 CAS。
• 概括范畴内容太少，可以写的更具体的。需要一个读过 Bart Jacobs 的人去写。
• 立方类型论可以直接搬运 https://ice1000.org/typst-workbench/cubicalmethods.pdf ，只是我一直没时间去做。
• 参数性中的内化一节。目前我并不认识掌握这方面知识、又会中文的人。可能是未来的我自己。
• 具现内容非常匮乏。可以考虑和有效意象联系起来。