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

[Jacques Carette]

Given an arbitrary Set (type) A, is it possible to express that a type 
such as "A → ℤ" is finitely supported?  The context is that of defining 
a free abelian group, so I need to define a concept of Direct Sum.  I 
would prefer, if at all possible, to make no assumptions on A.

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.  In other places, I have seen people use 
the existence of an induction principle as a proxy for finiteness [but 
they also assumed a decidable equivalence on A].

Jacques