我只是个普通人，并不真正了解 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 中将整数定义为商的定义，但我找不到这种运算的定义位置。