在HIT上定义函数时，如何处理较高归纳的情况？

Question

我正在Agda中尝试同伦类型理论。我使用HIT定义整数：

{-# OPTIONS --cubical --safe #-}

open import Cubical.Foundations.Prelude
open import Data.Nat using (?; _+_)

data ? : Set where
  -- | An integer i is a pair of natural numbers (m, n)
  --   where i = m - n
  int : ? ? ? ? ?
  -- | (a, b) = (c, d)
  --   a - b = c - d
  --   a + d = b + c
  int-eq : ? {a b c d : ?} ? (a + d ? b + c) ? int a b ? int c d

现在，我想在整数上定义加法：

add-ints : ? ? ? ? ?
add-ints (int a b) (int c d) = int (a + c) (b + d)

但是，编译器会出错，因为我还需要对匹配的相等构造函数进行模式匹配：

Incomplete pattern matching for add-ints. Missing cases:
  add-ints (int-eq x i) (int x? x?)
  add-ints x (int-eq x? i)
when checking the definition of add-ints

因此，我最终得到以下结果：

add-ints : ? ? ? ? ?
add-ints (int a b) (int c d) = int (a + c) (b + d)
add-ints (int-eq x i) (int c d) = { }0
add-ints (int a b) (int-eq x i) = { }1
add-ints (int-eq x i) (int-eq y j) = { }2

Agda的打孔无济于事：

?0 : ?
?1 : ?
?2 : ?

———— Errors ————————————————————————————————————————————————
Failed to solve the following constraints:
  ?0 (x = x) (i = i) (c = a) (d = b)
    = ?2 (x = x) (i = i) (y = x?) (j = i0)
    : ?
  ?0 (x = x) (i = i) (c = c) (d = d)
    = ?2 (x = x) (i = i) (y = x?) (j = i1)
    : ?
  ?1 (a = a?) (b = b?) (x = x?) (i = i)
    = ?2 (x = x) (i = i0) (y = x?) (j = i)
    : ?
  ?1 (a = c?) (b = d?) (x = x?) (i = i)
    = ?2 (x = x) (i = i1) (y = x?) (j = i)
    : ?
  int (a + x) (b + x?) = ?0 (x = x?) (i = i0) (c = x) (d = x?) : ?
  int (c + x) (d + x?) = ?0 (x = x?) (i = i1) (c = x) (d = x?) : ?
  int (x + a) (x? + b) = ?1 (a = x) (b = x?) (x = x?) (i = i0) : ?
  int (x + c) (x? + d) = ?1 (a = x) (b = x?) (x = x?) (i = i1) : ?

Agda文档提供了HIT用法的示例，其中在对圆环和命题截断进行操作时，它在相等构造函数上的模式匹配。但是，作为没有拓扑背景的人，我不会完全了解正在发生的事情。

iand j从[0，1]间隔开始的目的是什么，为什么它们出现在我的相等构造函数模式中？如何使用i和j？如何处理较高的归纳案例？

Answer 1

您可以将路径构造函数视为采用区间变量，并满足有关该区间端点的附加方程，

\n\n

data \xe2\x84\xa4 : Set where\n  int : \xe2\x84\x95 \xe2\x86\x92 \xe2\x84\x95 \xe2\x86\x92 \xe2\x84\xa4\n  int-eq : \xe2\x88\x80 {a b c d : \xe2\x84\x95} \xe2\x86\x92 (a + d \xe2\x89\xa1 b + c) \xe2\x86\x92 I \xe2\x86\x92 \xe2\x84\xa4\n   -- such that int-eq {a} {b} {c} {d} _ i0 = int a b\n   -- and       int-eq {a} {b} {c} {d} _ i1 = int c d\n

\n\n

在 int-eq 的加整数方程中，您还必须生成 \xe2\x84\xa4，并且它必须与第一个子句匹配（对于int在两个端点处匹配第一个子句（对于构造函数）。这些是 Agda 报告的限制，称不同的条款必须达成一致。

\n\n

您可以先从 ?0 开始。对于这一点，只有最后两个约束很重要。它有助于填写隐式变量，

\n\n

add-ints (int-eq {a0} {b0} {a1} {b1} x i) (int c d) = { }0\n

\n\n

为了匹配第一个子句，您需要提供一个 \xe2\x84\xa4 类型的值，该值等于int (a0 + c) (b0 + d)wheni = i0且等于int (a1 + c) (b1 + d)when i = i1。您可以使用int-eq为此使用构造函数，

\n\n

?0 = int-eq {a0 + c} {b0 + d} {a1 + c} {b1 + d} ?4 i\n

\n\n

必须算出等式?4。

\n