[Agda] 'finitely supported' constructively and without decidable equality

[Nils Anders Danielsson]

On 2016-12-30 16:02, Jacques Carette wrote:
> I have used
>     B : Pred A o
>     finite : Σ ℕ (λ n → (Σ A B ↣ Fin n))
>
> to define a "finitely supported subset of A" which 'works', but is
> extremely awkward to work with.

Is A an h-set, and is B h-propositional?

-- 
/NAD