Q: The set of all elements of a type

Stream: maths

[Mark Fischer]

For any type α, I can talk about sets of the type — ie. Set α.

Say I have t : Set α such that ∀(a:α), a ∈ t,
Does t have a name in type/set theory?

[Graham Leach-Krouse]

Perhaps "the universal set (of α)"? For example: https://leanprover-community.github.io/mathlib4_docs/Mathlib/Init/Set.html#Set.univ

[Mark Fischer]

Isn't that a type rather then a set?

[Mark Fischer]

t : {_a : α | True} is a proof that the type in inhabited, not the set of all elements of α?

[Mark Fischer]

t : Set {_a : α | True} is almost just t : Set α... I think

[Kevin Buzzard]

Set.univ is a term of type Set \alpha, not a type.

[Graham Leach-Krouse]

Are you perhaps thinking of subtype notation? {x : α // p x} gives you a type (intuitively - really it's dependent pairs) inhabited by the things of type α that satisfy p.

[Kevin Buzzard]

t : {_a : α | True} doesn't make sense because {_a : α | True} is a term, not a type. Similarly t : Set {_a : α | True} doesn't make sense because Set wants to eat a type and you've given it a term. If these things are compiling in Lean then it's because Lean is inserting coercions, which are going to be muddying the water if you're trying to figure out what's going on under the hood.

[Mark Fischer]

Yeah, I was thinking of Subtype notation. You're right.

[Mark Fischer]

Follow up question, is there any machinery to automate the proof that a user defined inductive type is a Fintype?

That might be a hard problem. You'd need it to be a non-recursive inductive where every constructor uses only Fintypes as well.

[Kim Morrison]

@Treq, but in that easy case, just write deriving Fintype after the structure.

[Kyle Miller]

If you ever need to add additional assumptions, the module that defines deriving Fintype also provides derive_fintype% T, which you can use inside an instance with the additional instance arguments, like

instance ...arguments... : Fintype T := derive_fintype% _