# 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 `sorry`

s in the `Lean`

code. Once all these challenges are accomplished, you have established the above-mentioned isomorphism.