Zulip Chat Archive

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.