subject同伦类型论 [同伦类型论]

同伦类型论是一门新的提供数学基础的语言, 其自带的推理系统以及对类型 (特别是等式类型) 的 “空间” 解读使得它比经典逻辑下的集合论更接近于 $\infty$-意象内语言, 更能贴合同伦论的实践 (综合同伦论).