agda - 在 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.但是，作为没有拓扑背景的人，我并不完全了解正在发生的事情。
i的目的是什么？和 j来自 [0, 1] 区间，为什么它们会出现在我的等式构造函数模式中？我如何使用 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-int 的方程中，您还必须生成一个 ℤ，并且它必须匹配两个端点的第一个子句(对于 int 构造函数)。这些是 Agda 报告的约束，说不同的条款必须达成一致。

您可以先从 ?0 开始。对于其中只有最后两个约束重要。它有助于在这里填充隐式变量，

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

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

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

必须计算出等式 ?4。