homotopy-type-theory
-
展开在 Coq 中使用 `assert` 创建的术语
-
你如何在 Cubical Agda 中使用 Ring 求解器？
-
如何在 coq 中明确使用归纳原理？
-
这个 Modulo a Set 的公式是什么？
-
我可以在 Cubical Agda 中使用归纳类型族吗？
-
我们可以在没有模式匹配的情况下（仅使用 J 和 K）在 Agda 中推导出 Equality/Identity 证明的唯一性吗？
-
在不写出所有定律的情况下表示同态
-
有限多重集作为 Cubical Agda 中的 HIT
-
在 isSet 类型中构建具有约束的正方形
-
在 isSet 类型中构建具有约束的路径
-
内涵类型理论之上的定义和命题外延性是否等价？
-
区间外延性？
-
单价公理是内射的吗？
-
路径之间的平等
-
在 Cubical 模式下定义非一元函数
-
使用 eq_rect 的路径归纳
-
同伦类型理论和 Voevodsky 的单价基础一文的 coq 代码
-
COQ 和 HOTT 中平等定义的原因
-
如何在 Agda 中使用 N 的归纳原理证明 N 的递归定义方程命题成立？