Доказывая разрешимость подмножества в Agda

Question

Пусть у меня есть такое определение подмножества в Agda

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

и у меня есть набор

data Q : Set where 
a : Q 
b : 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

Не для этого определения подмножества, так как разреши потребуется, чтобы проверить, является ли «р а» населена или нет, то есть без середины.

Разрешимые подмножества будут точно быть карты в Bool:

Но если вы хотите больше гибкости в форме членства доказательств можно использовать определение подмножества и носить с собой доказательство того, что она разрешима.