title: How to encode via W-types in agda?
body: <p>I'm trying to encode lists via W-types in Agda, when trying to prove my encoding correct, I get the following unsolveable goal.</p>
  <pre><code>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
  </code></pre>
  <p>I assume that when defining my forward function in the equivalance, <code>f (sup (inr a) x) = a ∷ f (x a)</code> , needs to somehow not just apply x to a, but I don't see how to do this.  Otherwise, am I defning by <code>B x</code> wrong, or is there some other minor error in backwards function, <code>g</code>?  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.</p>
  <pre><code>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')!}))
  </code></pre>