Quotient

A quotient of a set $X$ by an equivalence relation $\sim :X\to X\to \mathrm{Prop}$ is a unique set $[X{]}_{\sim }\subseteq \mathcal{P}X$ such that,

• $[X{]}_{\sim }$ partitions $X$
• $[x{]}_{\sim }=[y{]}_{\sim }$ iff $x\sim y$ for all $x,y\in X$.