Partition of a Set

A partition of a set $X$ is a set of subsets $P\subset\mathcal{P}(()X)$ such that:

• $\emptyset\notin P$
• $\bigcup P=X$
• If $A\in P$ and $B\in P$, then $A\cap B=\emptyset$.

Alternatively, a partition on $X$ is an Equivalence Relation $\approx$ with an attitude; instead of viewing $\approx$ as an alternative equivalence relation, we consider the type Singletons with respect to $\approx$; EG: $Sing(x)=\Sigma(y:X).\;x\approx y$