类型论、同伦类型论与形式化数学，研究数学陈述与证明本身的结构。
本领域共 1 个概念。
同伦类型论把类型解释为空间、项解释为点、等词类型 a = A b 解释为道路空间； 在此解释下同伦等价对应类型等价，Voevodsky 的单价公理使「等价即相等」成为可形式化的原则。