在 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) : ℤ

The Agda documentation gives examples of HIT usage, where it pattern matches on the equality constructors when operating on the torus and propositional truncation. 但是，作为一个没有拓扑学背景的人，我并不完全了解正在发生的事情。

[0, 1] 区间中的i 和j 的用途是什么，为什么它们会出现在我的等式构造函数模式中？如何使用i 和j？如何处理较高归纳的情况？

Answer 1

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

data ℤ : Set where
  int : ℕ → ℕ → ℤ
  int-eq : ∀ {a b c d : ℕ} → (a + d ≡ b + c) → I → ℤ
   -- such that int-eq {a} {b} {c} {d} _ i0 = int a b
   -- and       int-eq {a} {b} {c} {d} _ i1 = int c d

在 int-eq 的 add-ints 的方程式中，您还必须生成一个 ℤ，并且它必须匹配两个端点的第一个子句（对于 int 构造函数）。这些是 Agda 报告的约束，表示不同的条款必须达成一致。

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

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

要匹配第一个子句，您需要得出一个 ℤ 类型的值，当 i = i0 时等于 int (a0 + c) (b0 + d)，当 i = i1 时等于 int (a1 + c) (b1 + d)。您可以为此使用int-eq 构造函数，

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

等式 ?4 必须计算出来。