请求立方Agda中整数HIT加法运算的实现示例

前置准备：自然数加法的基本引理 #

首先需要定义自然数加法的交换律和结合律，这些是构造整数商等式的核心基础：

open import 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)

-- 自然数加法交换律
commN : (m n : N) → m +N n ≡ n +N m
commN 0N n = refl
commN (suc m) n = cong suc (commN m n)

-- 自然数加法结合律
assocN : (m n k : N) → (m +N n) +N k ≡ m +N (n +N k)
assocN 0N n k = refl
assocN (suc m) n k = cong suc (assocN m n k)

-- 等式推理语法糖
open import Cubical.Core.Path using (_≡⟨_⟩_; _∎)

整数的商定义 #

用自然数对的商来定义整数，等价关系为(a,b) ≡ (c,d) 当且仅当 a+d = b+c：

data Z : Set where
  zpair : N → N → Z
  zeq : (a b c d : N) → (a +N d ≡ b +N c) → zpair a b ≡ zpair c d

整数加法的完整实现 #

下面是整数加法_+Z_的定义，包含基础情况、单路径参数情况，以及你困惑的双路径参数情况：

_+Z_ : Z → Z → Z
-- 基础情况：两个自然数对直接相加
zpair a b +Z zpair c d = zpair (a +N c) (b +N d)

-- 单路径参数情况：固定自然数对 + 等价路径
zpair a b +Z zeq e f g h q j =
  let
    -- 证明(a+e)+(b+h) ≡ (b+f)+(a+g)，满足等价关系
    sum-equiv : (a +N e) +N (b +N h) ≡ (b +N f) +N (a +N g)
    sum-equiv =
      (a +N e) +N (b +N h) ≡⟨ sym (assocN a e (b +N h)) ⟩
      a +N (e +N (b +N h)) ≡⟨ cong (λ x → a +N x) (sym (assocN e b h)) ⟩
      a +N ((e +N b) +N h) ≡⟨ cong (λ x → a +N (x +N h)) (commN e b) ⟩
      a +N ((b +N e) +N h) ≡⟨ cong (λ x → a +N x) (assocN b e h) ⟩
      a +N (b +N (e +N h)) ≡⟨ assocN a b (e +N h) ⟩
      (a +N b) +N (e +N h) ≡⟨ cong (λ x → (a +N b) +N x) q ⟩
      (a +N b) +N (f +N g) ≡⟨ sym (assocN a b (f +N g)) ⟩
      a +N (b +N (f +N g)) ≡⟨ cong (λ x → a +N x) (sym (assocN b f g)) ⟩
      a +N ((b +N f) +N g) ≡⟨ cong (λ x → a +N (x +N g)) (commN b f) ⟩
      a +N ((f +N b) +N g) ≡⟨ cong (λ x → a +N x) (assocN f b g) ⟩
      a +N (f +N (b +N g)) ≡⟨ cong (λ x → a +N (f +N x)) (commN b g) ⟩
      a +N (f +N (g +N b)) ≡⟨ cong (λ x → a +N x) (sym (assocN f g b)) ⟩
      a +N ((f +N g) +N b) ≡⟨ sym (assocN a (f +N g) b) ⟩
      (a +N (f +N g)) +N b ≡⟨ cong (λ x → x +N b) (sym (assocN a f g)) ⟩
      ((a +N f) +N g) +N b ≡⟨ cong (λ x → (x +N g) +N b) (commN a f) ⟩
      ((f +N a) +N g) +N b ≡⟨ assocN f a g ⟩
      (f +N (a +N g)) +N b ≡⟨ sym (assocN f (a +N g) b) ⟩
      f +N ((a +N g) +N b) ≡⟨ cong (λ x → f +N x) (commN (a +N g) b) ⟩
      f +N (b +N (a +N g)) ≡⟨ assocN f b (a +N g) ⟩
      (f +N b) +N (a +N g) ≡⟨ cong (λ x → x +N (a +N g)) (commN f b) ⟩
      (b +N f) +N (a +N g) ∎
  in
    zeq (a +N e) (b +N f) (a +N g) (b +N h) sum-equiv j

-- 双路径参数情况：两个等价路径相加
zeq a b c d p i +Z zeq e f g h q j =
  let
    -- 定义四个角的加法结果
    top-left = zpair (a +N e) (b +N f)
    top-right = zpair (a +N g) (b +N h)
    bottom-left = zpair (c +N e) (d +N f)
    bottom-right = zpair (c +N g) (d +N h)

    -- 上边路径：top-left → top-right（对应j变化，i固定为0）
    top-path = zpair a b +Z zeq e f g h q
    -- 左边路径：top-left → bottom-left（对应i变化，j固定为0）
    left-path = zeq a b c d p +Z zpair e f
    -- 右边路径：top-right → bottom-right（对应i变化，j固定为1）
    right-path = zeq a b c d p +Z zpair g h
    -- 下边路径：bottom-left → bottom-right（对应j变化，i固定为1）
    bottom-path = zpair c d +Z zeq e f g h q
  in
    hfill (λ k → λ {
      (i = i0) → top-path (j ∧ k);
      (i = i1) → right-path (j ∧ k);
      (j = i0) → left-path (i ∧ k);
      (j = i1) → bottom-path (i ∧ k)
    }) (inS top-left) (i ∨ j)

关键说明 #

• 双路径参数的本质是构造二维路径（立方体），需要保证四条边缘的路径都符合加法的定义。
• hfill是Cubical Core库中的工具，用于填充由四条路径围成的正方形：
  • 第一个参数描述四条边界在任意填充进度k下的取值
  • inS top-left指定填充的起始点
  • i ∨ j控制填充方向，最终返回任意(i,j)对应的整数元素
• 所有等价性证明都依赖自然数加法的交换律和结合律，这是商结构保持运算的核心要求。

内容的提问来源于stack exchange，提问作者Louis Wasserman