初见同伦类型论

最近找到了一个研究类型论的群体，主要是数学系的，看到他们对同伦类型论和立方类型论比较感兴趣。我虽然是一个傻逼计科人，但至少我也会普通的依值类型论（虽然可能不太能用数学语言表述出来），而且最近也做出了一些输出（例如写了依值类型的 typecheck，用 linear types 尝试构造了一种可自定义的程序生成方式），或许是时候吸收一些新的知识了。

同伦类型论里面结合了数学里面各类奇妙领域的东西，例如拓扑学、范畴论之类的东西，我似乎都完全不知道，但无所谓。似乎同伦类型论主要是用于解决 Martin-Löf 类型论中「类型」本身定义不明确的问题，进而能够更好地对「相等关系」之类的抽象实体进行建模。

神秘的类比

一般而言在正常类型论里面的 “a : A” 会被解读成 a 在 A 这个集合中，但在同伦类型论中因为有拓扑学的成分，被解释成 a 在 A 这个「空间」中。我一直对类型的解读是类型是「位置」，但由于同一类型显然可以有各种不同的实例，我直觉上觉得确实说是「空间」更加恰当。

他说空间是「无穷基本群胚」，我觉得很抽象。但这个空间里面的「路径」我暂时无法把它和拓扑学对应起来。这个路径连续与否要怎么判断呢？

怎么还出来了「CW 复形」？死都看不懂……拓扑一点不会！怎么学个编程还要学拓扑？

神秘定理

现在使用传统 dependent type 证明某些东西不可避免使用 Axiom of Choice 或者 Law of Excluded Middle, 但使用 HoTT 可以在部分场景下避免对这俩的使用。至于在 inductive datatypes 下是不是总能避免使用这俩，则是一个开放问题。

同时，对于离散的 inductive datatypes 的处理，例如自然数，似乎也存在开放问题。

前置

从知乎上复制一段学习 HoTT 的前置知识：

1：数学中代数/拓扑/代数拓扑/范畴论的知识 

2：计算机/逻辑中类型论相关知识

关于1，非数学系本科需要再学高级版线性代数（高等代数），推荐linear algebra done right,然后看抽象代数，springer gtm系列里边找（推荐hungerford那本)，然后是点集拓扑（推荐munkres第一部分的），最后是代数拓扑（hatcher)。为了强化下范畴论，再看看rotman的同调代数

2：熟悉Haskell,agda, idris等语言，对于函数式编程要非常熟练，基本算法都能用Haskell写出来，然后能用dependent type证明简单定理。

作者：Martin awodey
链接：https://www.zhihu.com/question/311127230/answer/589239343
来源：知乎
著作权归作者所有。商业转载请联系作者获得授权，非商业转载请注明出处。

我 2 会，1 只完成了高等代数，悲。但是先不管了，先看看 HoTT Book 再说。

Tip

深圳中学有教 HoTT 的社团。