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