Agda中子集可判定性的证明

Question

假设我在Agda中有子集的定义

Subset : ∀ {α} → Set α → {ℓ : Level} → Set (α ⊔ suc ℓ)
Subset A {ℓ} = A → Set ℓ

我有一套

data Q : Set where
 a : Q
 b : Q

能证明q的所有子集都是可判定的吗?为什么？

Qs? : (qs : Subset Q {zero}) → Decidable qs

可决定的定义如下：

-- Membership
infix 10 _∈_
_∈_ : ∀ {α ℓ}{A : Set α} → A → Subset A → Set ℓ
a ∈ p = p a

-- Decidable
Decidable : ∀ {α ℓ}{A : Set α} → Subset A {ℓ} → Set (α ⊔ ℓ)
Decidable as = ∀ a → Dec (a ∈ as)

Answer 1

对于子集的这一定义不是这样，因为可判定性将需要检查是否有人居住"p“，即排除中间。

可决策子集将准确地映射到Bool：

Subset : ∀ {α} (A : Set α) -> Set
Subset A = A → Bool 

_∈_ : ∀ {α}{A : Set α} → A → Subset A → Set
a ∈ p = T (p a)

但是如果你想在成员证明的形状上有更多的灵活性，你可以使用子集的定义来证明它是可决定的。