All finite types are small.

That is, any α with [Fintype α] is equivalent to a type in any universe.

instance small_of_fintype (α : Type v) [Fintype α] : Small.{w, v} α

Equations

• (_ : Small.{w, v} α) = (_ : Small.{w, v} α)