CODEWITHSUNDEEP
typesfunctional-programmingagdainduction
user5775230
user5775230

Reputation:

How to encode via W-types in agda?

I'm trying to encode lists via W-types in Agda, when trying to prove my encoding correct, I get the following unsolveable goal.

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

I assume that when defining my forward function in the equivalance, f (sup (inr a) x) = a ∷ f (x a) , needs to somehow not just apply x to a, but I don't see how to do this. Otherwise, am I defning by B x wrong, or is there some other minor error in backwards function, g? How does one approach debugging this? I can provide all the code used, but I'm hoping the error can be spotted by eye for brevity. Also note, λ≡ denotes function extensionality.

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')!}))

Upvotes: 2

Views: 275

Answers (1)

user5775230
user5775230

Reputation:

As pointed out by @HTNW , the way you encode arity indexing type is the same as for the natural numbers, thus it is only the Base Type over which serves as the index data. Thus, the modification below allows the proof to go through smoothly.

It's easy to get confused as to how the data should be ecoded into the Well-order constructor, and therefore lends itself to seemingly simple mistakes.

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')))

Upvotes: 3

Related Questions