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

[Thorsten Altenkirch]

I think this is also equivalent to the definition I gave.

data IsFin : Set → Set where
	empty : IsFin ⊥
	suc : ∀ {A} (a : A) → IsFin (A - a) → IsFin A

If you want to avoid giving an ordering there is the following alternative:


data Noeth : Set → Set where
	noeth : ∀ {A} → ((a : A) → Noeth (A - a)) → Noeth A

Thorsten


P.S. Agda file attached.


On 10/01/2017, 18:21, "Agda on behalf of Twan van Laarhoven"
<agda-bounces at lists.chalmers.se on behalf of twanvl at gmail.com> wrote:

>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
>_______________________________________________
>Agda mailing list
>Agda at lists.chalmers.se
>https://lists.chalmers.se/mailman/listinfo/agda





This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please send it back to me, and immediately delete it. 

Please do not use, copy or disclose the information contained in this
message or in any attachment.  Any views or opinions expressed by the
author of this email do not necessarily reflect the views of the
University of Nottingham.

This message has been checked for viruses but the contents of an
attachment may still contain software viruses which could damage your
computer system, you are advised to perform your own checks. Email
communications with the University of Nottingham may be monitored as
permitted by UK legislation.

-------------- next part --------------
A non-text attachment was scrubbed...
Name: finteShort.agda
Type: application/octet-stream
Size: 381 bytes
Desc: finteShort.agda
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20170110/36dfdd68/attachment-0001.obj>