Open claims for partitions of finite types

[fredrik-bakke]

The following claims remain to be formalized in univalent-combinatorics.partitions:

• The type of finite partitions of a finite type X is equivalent to the type of decidable partitions of X in the usual sense
• The type of finite partitions of a finite type X is equivalent to the type of equivalence relations on X
• The type of finite partitions of a finite type is finite
• The number of elements of the type of finite partitions of a finite type is a Stirling number of the second kind
• The type of finite partitions of a contractible type is contractible