Доказательство разрешимости подмножества в Агде

Question

Предположим, у меня есть это определение Подмножество в Агде

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

Decidable определяется здесь:

-- 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

Не для этого определения Подмножества, так как для принятия решения потребуется проверить, обитаем ли "pa" или нет, то есть исключен средний.

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

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

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

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