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

Question

#### Exercise `Any-∃`

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

撇开∃[ x ∈ xs ] P x甚至不是有效语法的事实不谈- 只有Σ[ 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 书的列表章节中的倒数第二个练习。

标签： agdaplfa

Answer 1