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

[Twan van Laarhoven]

You could consider using a `List A` as a finite subset of A, so things like

   record FiniteSupport {A : Set} (f : A → ℤ) where
     field support : List A
     field unsupported : ∀ {x} → x ∉ support → f x ≡ 0

And finite sets would be:

   record Finite (A : Set) where
     field enum : List A
     field member : ∀ x → x ∈ enum
     -- optional:
     field unique : ∀ {x} → (x∈enum : x ∈ enum) → x∈enum ≡ member x

This is slightly stronger than just knowing that a type is finite, since you 
also get an ordering of the elements, but you also get this from a bijection 
with Fin.

Twan

On 2016-12-30 16:02, Jacques Carette wrote:
> 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
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda