## Stream: general

### Topic: converting a finset to a Type

#### Scott Morrison (Aug 06 2019 at 07:24):

Is it possible to convert a finset into a type in an arbitrary (possibly smaller) universe, in the following sense:

universes u v

def finset.index_type {α : Type u} (s : finset α) : Type v := sorry
def finset.index_equiv {α : Type u} (s : finset α) : s.index_type ≃ { a // a ∈ s } := sorry


If we replace the return type with Type u it is of course possible:

def finset.index_type {α : Type u} (s : finset α) : Type u := { a // a ∈ s }
def finset.index_equiv {α : Type u} (s : finset α) : s.index_type ≃ { a // a ∈ s } := by refl


But my intuition is that since we know s is finite, we should be able to change universes willy-nilly. Any ideas?

#### Scott Morrison (Aug 06 2019 at 07:26):

I want to do something like define index_type as fin n for the appropriate n, but then .... use trunc in some clever way to allow defining the equivalence.

#### Johan Commelin (Aug 06 2019 at 07:27):

Can't you make an inductive type?

Let me try

#### Johan Commelin (Aug 06 2019 at 07:30):

Hmm, no, that will always land in Type (max u v) I guess

#### Johan Commelin (Aug 06 2019 at 07:30):

So why don't you define it as fin s.card?

#### Chris Hughes (Aug 06 2019 at 07:33):

fin s.card?

#### Johan Commelin (Aug 06 2019 at 07:35):

@Scott Morrison Should the equivalence be somehow "canonical"? Or do you just want to choose one and work with it?

#### Johan Commelin (Aug 06 2019 at 07:39):

I guess, if you are allowed to choose a well ordering of α then it is possible.

#### Johan Commelin (Aug 06 2019 at 07:39):

Otherwise I don't really see how to do this.

#### Chris Hughes (Aug 06 2019 at 07:40):

It would be nice if it was computable. The defeq-ness might be handy

#### Chris Hughes (Aug 06 2019 at 07:41):

fintype.equiv_fin will help to define the bijection for s.card

#### Scott Morrison (Aug 06 2019 at 08:04):

Ah, thanks, equiv_fin should get me there.

Last updated: Dec 20 2023 at 11:08 UTC