lean::infinity:零地

零地 该库提供可计算的HIT，使用它们的Cubical Type Theory的变体以及其他一些数学运算。 命中率 （n截断除外）都是使用构造的。 精益中的商具有良好的计算属性（ quot.ind ），因此我们可以用它们来定义HIT，而不会在精益内核中进行任何其他更改。 有： 间隔。 推出去 。 同位实数 。 （顺序）限制。 广义圆。 整数 。 有理数 。 莫比乌斯乐队。 单面。 命题截断是以下序列的共限制： 暂停 定义为跨度的推出 。 圆圈 是布尔的悬浮液 。 领域 是圆的悬浮 。 加入。 立体类型理论（ 目录） 在拓扑函数中，从区间到某种类型的路径就是这种类型的路径。 在HoTT书中，路径类型被定义为具有一个构造函数的经典归纳类型： inductive eq {α : Sort u} (a : α) : α → Sort u | refl : eq