标签: 类型论

2021-05-11

从 Induction 到 Axiom K, UIP, J-rules

2020-10-28

奇妙的依赖类型 (上): 全类, $\Pi$-类型以及乘积类型

2020-10-11

Church-Rosser 定理证明

2020-09-27

不动点组合子的原理与定理证明

2020-09-21

Lambda 立方体与类型系统简记