HoTT讨论版课堂笔记-1

人民大学同伦类型论讨论班，今天举行了第一次聚会。我使用手机拍照了一些有意思的板书，权当做笔记，希望对未来者学习有帮助，也作为自己继续学习、查找资料的参考。

今天的主讲人是孙振宇与朱俸民。孙振宇是现场板书，朱俸民远程使用agda现场敲代码。拍照的内容属于哪位老师/同学，大家一看便知。

HoTT跟三门学科有关系，即：类型论、Higher Topos Theory, 同论论。Topos 理论完全没有学过，不懂。我记得HoTT Book 说的是这个理论跟类型论、代数拓扑学、范畴论都有关系。

这里提到了G神的猜想,就是图中右上角的"space=sigma-groupoid".据说这个猜想接近完成了。

第一个式子描述的把一个lambda函数这样的term应用到另一个term 的运算规则，也就是所谓的beta rule.这是在讲某个形式语言（比如simply typed theory或者其它更复杂的type theory中）的某个“语义”，即“计算”。

式子中的三个横线意思是“定义为”。

第二个式子是讲所谓的eta rule.对于一个函数类型的term 来说，它一定可以表示为lambda抽象类型这种term，其中的phi是一个未知的表达式。

HoTT本身是一个形式语言，只是比最简单的Simply Typed Theory复杂而已。这里讲了要HoTT中的identity type “解释”为代数拓扑学中的拓扑空间中的两点之间的路径（从区间[0, 2]到这两个点的一个连续映射）。

我原来的记忆是把identity type解释为路径的同论等价类。需要继续查一下资料。

怎么定义的Eq(A, B)?

这里提到的公理就是Vladimir Voevodsky提出的univalence axiom.这是HoTT两大创新点之一。

这里又讲到了HoTT的第二大创新点Higher Inductive Type.

MiniTT指的具体是Per Martin Lof的内涵类型论的修改版？

Higher Inductive Type 其实就是CW Complex.惭愧当年没学过CW Complex.

一族“类型”（空间）是什么意思？

跟空间的fibration有关系。问题是fibration是什么？

h levels 是什么？