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