Quotient

Definition

The set quotient $A/R$ is a quotient inductive type that quotients a type $A$ by a relation $R:A\to A\to \mathcal{U}$ and truncates the resulting type to a hSet.

Given a type $A$ and a relation $R:A\to A\to \mathcal{U}$, the set quotient $A/R$ has the following constructors:

• $|\_|:A\to A/R$
• $\mathrm{eq}:\Pi (x,y:A).Rxy\to |x|=|y|$
• $\mathrm{isSet}:\Pi (x,y:A/R).\Pi (p,q:x=y).(p=q)$

The first constructor embeds elements of $A$ into the quotient. The second constructor identifies elements that are related by $R$. The third constructor ensures that the quotient is a set by requiring that all parallel paths are equal.

Properties

Effectiveness: If $R$ is an equivalence relation, then $|x|=|y|$ implies that $Rxy$. Truncation: The set quotient is a hSet (set) by construction, due to the $\mathrm{isSet}$ constructor which is a truncation constructor.

Remarks

The set quotient does not require $R$ to be an equivalence relation a priori, though in practice it is often used with equivalence relations.

Without the set truncation, it is not garunteed that there is a unique path between any two elements, instead you get the free infinity groupoid.

Related Concepts

Higher Inductive Type Quotient Inductive Type hSet Truncation (HoTT) Equivalence Relation