fintype α means that α is finite, i.e. there are only finitely many distinct elements of type α. The evidence of this is a finset elems (a list up to permutation without duplicates), together with a proof that everything of type α is in the list.

univ is the universal finite set of type finset α implied from the assumption fintype α.

Construct a proof of fintype α from a universal multiset

Construct a proof of fintype α from a universal list

card α is the number of elements in α, defined when α is a fintype.

There is (computably) a bijection between α and fin n where n = card α. Since it is not unique, and depends on which permutation of the universe list is used, the bijection is wrapped in trunc to preserve computability.

Construct a fintype from a finset with the same elements.

If f : α → β is a bijection and α is a fintype, then β is also a fintype.

If f : α → β is a surjection and α is a fintype, then β is also a fintype.

If f : α ≃ β and α is a fintype, then β is also a fintype.

Construct a finset enumerating a set s, given a fintype instance.

bij_inv fis the unique inverse to a bijectionf. This acts as a computable alternative to function.inv_fun`.