Quotient set

In mathematics, the quotient set implements the notion of "equal modulo [something]."

Definition

Let $A$ be a set. A quotient of the set $A$ is a set $Q$ satisfying the following properties:

1. Every element of $Q$ is a non-empty subset of $A$

2. Any two distinct elements of $Q$ are disjoint subsets of $A$.

3. Every element of $A$ belongs to exactly one subset in $Q$.

Or, symbolically,

1. $\forall q\in Q,q\ne \varnothing \wedge q\subset A$

2. $\forall ab\in Q,a\cap b=\varnothing$

3. $\forall a\in A,\exists !q,a\in q$

A quotient set can be seen as a generalisation of a partion from two sets to some arbitrary cardinal.

Another way to view quotient sets is the set of equivalence classes for some relation on $A$. For any quotient set $Q$, you could define a relation $\sim$ by $\forall ab\in A,a\sim b⟺\pi a=\pi b$. This relation is symmetric, transitive, and reflexive; an equivalence relation.

Natural mapping

If $Q$ is a quotient set of $A$, then there is a unique surjection $\pi :A\to Q$ that sends each $a\in A$ to the 'bucket' to which it belongs in $Q$; that is, for every $a\in A$, $a\in \pi a$.

In a dependently-typed language, we would phrase this as