什么是“Any-∃”练习的有效类型签名？

Question

#### Exercise `Any-∃`

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

[不考虑∃[ x ∈ xs ] P x甚至不是valid syntax的事实-只有Σ[ x ∈ xs ] P x可能是有效的，我没有尝试过针对该特定问题进行类型检查的类型签名。

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

这里最明显的事情失败了。我有点理解问题在试图问我什么，但是我不确定∃[ x ∈ xs ] P x的结构应该是什么。

这是PLFA书籍Lists chapter中的倒数第二个练习。

Answer 1

该书现已更正：

练习Any-∃（练习）

[显示Any P xs与∃[ x ] (x ∈ xs × P x)同构。