Search code examples
agdaplfa

What is a valid type signature for the `Any-∃` exercise?

#### Exercise `Any-∃`

Show that `Any P xs` is isomorphic to `∃[ x ∈ xs ] P x`.

Leaving aside the fact that ∃[ x ∈ xs ] P x is not even valid syntax - only Σ[ x ∈ xs ] P x could be valid, none of the type signatures I've tried typecheck for that particular problem.

Any-∃ : ∀ {A : Set} {P : A → Set} {xs : List A} → Any P xs ≃ Σ[ x ∈ xs ] P x

List A !=< Set _a_1582 of type Set
when checking that the expression xs has type Set _a_1582

The most obvious thing here fails. I sort of understand what the question is trying to ask me here, but I am not sure what the structure ∃[ x ∈ xs ] P x is supposed to be.

This is the penultimate exercise in the Lists chapter of the PLFA book.

Solution

  • The book has been corrected now:

    Exercise Any-∃ (practice)

    Show that Any P xs is isomorphic to ∃[ x ] (x ∈ xs × P x).