如何在 agda 中通过 W 类型进行编码？

Question

我正在尝试通过 Agda 中的 W 类型对列表进行编码，在尝试证明我的编码正确时，我得到了以下无法解决的目标。

Goal: g (f (x a)) ≡ x a'
Have: g (f (x a')) ≡ x a'
————————————————————————————————————————————————————————————
a' : A
x  : A → W (⊤ ⊔ A) Blist
a  : A
A  : Type

我假设在等价中定义我的前向函数时，f (sup (inr a) x) = a ∷ f (x a) 需要以某种方式不仅将 x 应用于 a，但我不知道如何做到这一点。否则，我定义的B x 是错误的，还是在向后函数g 中存在其他一些小错误？一种方法如何调试这个？我可以提供所有使用的代码，但为了简洁起见，我希望可以通过眼睛发现错误。另请注意，λ≡ 表示函数可扩展性。

data W (A : Type) (B : A → Type) : Type where
  sup : (a : A) → ((b : B a) → W A B) → W A B


Blist : ∀ {A} → ⊤ ⊔ A → Type
Blist (inl x) = ⊥
Blist {A} (inr x) = A

List' : Type → Type
List' A = W (⊤ ⊔ A) Blist

data List (A : Type) : Type where
  [] : List A
  _∷_ : A → List A → List A

ListsEquiv : ∀ {A} → List' A ≃ List A
ListsEquiv {A} = equiv f g fg gf
  where
    f : List' A → List A
    f (sup (inl top) x) = []
    f (sup (inr a) x) = a ∷ f (x a)
    g : List A → List' A
    g [] = sup (inl tt) abort
    g (a ∷ as) = sup (inr a) λ a' → g as
    fg : (y : List A) → f (g y) ≡ y
    fg [] = refl
    fg (x ∷ y) = ap (λ - → x ∷ -) (fg y)
    gf : (x : List' A) → g (f x) ≡ x
    gf (sup (inl tt) x) = ap (λ - → sup (inl tt) -) (λ≡ (λ x₁ → abort x₁))
    gf (sup (inr a) x) = ap (λ - → sup (inr a) -) (λ≡ (λ a' → {!gf (x a')!}))

Answer 1

正如@HTNW 所指出的，您对arity 索引类型进行编码的方式与自然数相同，因此只有Base Type 用作索引数据。因此，下面的修改可以让证明顺利通过。

对于如何将数据编码到 Well-order 构造函数中很容易感到困惑，因此容易出现看似简单的错误。

Blist : ∀ {A} → ⊤ ⊔ A → Type
Blist (inl x) = ⊥
Blist (inr x) = ⊤

List' : Type → Type
List' A = W (⊤ ⊔ A) Blist


ListsEquiv : ∀ {A} → List' A ≃ List A
ListsEquiv {A} = equiv f g fg gf
  where
    f : List' A → List A
    f (sup (inl top) x) = []
    f (sup (inr a) x) = a ∷ f (x tt)
    g : List A → List' A
    g [] = sup (inl tt) abort
    g (a ∷ as) = sup (inr a) λ a' → g as
    fg : (y : List A) → f (g y) ≡ y
    fg [] = refl
    fg (x ∷ y) = ap (λ - → x ∷ -) (fg y)
    gf : (x : List' A) → g (f x) ≡ x
    gf (sup (inl tt) x) = ap (λ - → sup (inl tt) -) (λ≡ (λ x₁ → abort x₁))
    gf (sup (inr a) x) = ap (λ - → sup (inr a) -) (λ≡ (λ a' → gf (x a')))