主页 / coding / 问题 / 79157635
Accepted
Louis Wasserman
Asked: 2024-11-05 11:48:43 +0800 CST

定义 HIT 上的操作

  • 772

我只是个普通人，并不真正了解 Cubical Agda 的所有细节。我曾尝试阅读其文档和 HoTT，但很快就不再关注发生了什么。

我特别希望的是一个如何为更高归纳类型编写简单操作的示例，理想情况下不需要外部库Cubical.Core.Everything。

举一个具体的例子，我们将整数视为自然数对的商：

data N : Set where
  0N : N
  suc : N -> N

_+N_ : N -> N -> N
0N +N n = n
suc m +N n = suc (m +N n)

data Z : Set where
  zpair : N -> N -> N
  zeq : (a b c d : N) -> (a +N d) === (b +N c) -> zpair a b === zpair c d

_+Z_ : Z -> Z -> Z
zpair a b + zpair c d = zpair (a +N c) (b +N d)
zeq a b c d ad=bc i + zeq e f g h eh=fg j = ???

zpair + zeq我可以并且已经通过例如和反之亦然的方式工作，其中有一个i : I和我可以构建一条适当的路径并将其应用于i。我不明白当我有i j : I和我将路径上的点组合在一起时该怎么做，特别是看起来我不能将它们楔在一起，也没有看到明显的组合或将I其应用于的值。

令人满意的答案将填写???，假设上有任何必要的方便引理_+N_，并根据需要使用方程推理 API。

我查看了 Agda 中将整数定义为商的定义，但我找不到这种运算的定义位置。

agda

1 个回答

  1. Best Answer

    通常的方法是添加一个集合截断构造函数，例如

      squash : isSet Z

    这确保你可以填充 中的任何方块Z，例如使用isSet→SquareP。（请注意，isSet Z展开为具有正确形状的东西，可以用作更高级构造函数的类型。）

    您可以在这里的立方体库中看到这种方法的实际效果：注意，被定义为某种关系的ℤ商，其中商被定义为更高的归纳类型，并带有一个强制商为集合的构造函数。ℕ × ℕrelsquash/

    有关不需要截断的另一种方法，请参阅1lab：这里我们将路径构造函数限制为形式为 (x, y) 和 (x + 1, y + 1) 的相关对。您可以确信这不会引入任何非平凡循环，因此生成的 HIT 是一个集合（首先将 ℕ × ℕ 绘制为网格，然后在每对通过路径相关的点之间画一条线；您看到这与以前的方法有何不同吗？）。

    一旦完成，通常通过为整数定义递归原理来抽象出实现的细节，如果我们假设目标类型是较低的 h 级（在本例中为集合），则它通常可以具有更简单的形式。

    • 1

相关问题