我正在 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 用法的示例,它在对环面和命题截断进行操作时在等式构造函数上进行模式匹配。但是,作为没有拓扑学背景的人,我并不完全了解正在发生的事情。
i
[0, 1] 区间的and的目的是什么j
,为什么它们会出现在我的相等构造函数模式中?如何使用i
和j
?我如何处理较高归纳的情况?