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