Homework (IX)

Problem 1

In the following file we prove that equivalence relations and partitions are the same thing by constructing an isomorphism between the type of equivalence relations and the type of partitions.

There are few Challenges in the file below each involving filling in for sorrys in the Lean code. Once all these challenges are accomplished, you have established the above-mentioned isomorphism.