在Agda中证明广义复合mapₙ伪结合律的类型检查难题

背景 #

我正在将论文《Continuation-Passing Style, Defunctionalization, Accumulations, and Associativity》从Idris迁移至Agda。论文最终示例里的广义复合等价于Function.Nary.NonDependent.Base中的mapₙ函数，我需要证明它的伪结合律。

尝试的定理类型（类型检查失败） #

我写出了期望的定理类型，但代码无法通过类型检查：

mapₙ-assoc : ∀ {n m : ℕ} {ls ls′ r s t} {x : Set r} {y : Set s} {z : Set t} {as : Sets n ls} {bs : Sets m ls′}
  → (h : y → z) → (g : Arrows (suc m) (x , bs) y) → (f : Arrows n as x)
  → mapₙ n (mapₙ (suc m) h g) f ≡ mapₙ (n + m) h (mapₙ n g f)

报错信息：

n != n + m of type ℕ
when checking that the expression mapₙ n g f has type _as_1119 ⇉ y

自然数归纳版本（无法完成归纳步骤） #

我尝试了按自然数归纳定义的版本，该版本对任意特定n值均有效，但我无法完成归纳步骤，也无法让Agda确认通用n情况下的类型相等：

mapₙ-assoc : ∀ {n m : ℕ} {ls ls′ r s t} {x : Set r} {y : Set s} {z : Set t} {as : Sets n ls} {bs : Sets m ls′}
  → (h : y → z) → (g : Arrows (suc m) (x , bs) y) → (f : Arrows n as x) → Set _
mapₙ-assoc {zero} {m} h g f = mapₙ zero (mapₙ (suc m) h g) f ≡ mapₙ (zero + m) h (mapₙ zero g f)
mapₙ-assoc {suc n} {m} h g f = {!!}

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