# 6.10 Quotients

A particularly important sort of colimit of sets is the quotient  by a relation   . That is, let $A$ be a set and $R:A\times A\to\mathsf{Prop}$ a family of mere propositions (a mere relation). Its quotient should be the set-coequalizer of the two projections  $\mathchoice{{\textstyle\sum_{(a,b:A)}}}{\sum_{(a,b:A)}}{\sum_{(a,b:A)}}{\sum_{% (a,b:A)}}R(a,b)\rightrightarrows A.$

We can also describe this directly, as the higher inductive type $A/R$ generated by

• A function $q:A\to A/R$;

• For each $a,b:A$ such that $R(a,b)$, an equality $q(a)=q(b)$; and

• The $0$-truncation constructor: for all $x,y:A/R$ and $r,s:x=y$, we have $r=s$.

We may sometimes refer to $A/R$ as the set-quotient of $A$ by $R$, to emphasize that it produces a set by definition. (There are more general notions of “quotient” in homotopy theory, but they are mostly beyond the scope of this book. However, in §9.9 (http://planetmath.org/99therezkcompletion) we will consider the “quotient” of a type by a 1-groupoid, which is the next level up from set-quotients.)

###### Remark 6.10.1.

It is not actually necessary for the definition of set-quotients, and most of their properties, that $A$ be a set. However, this is generally the case of most interest.

###### Proof.

We must show that for any $x:A/R$ there merely exists an $a:A$ with $q(a)=x$. We use the induction  principle of $A/R$. The first case is trivial: if $x$ is $q(a)$, then of course there merely exists an $a$ such that $q(a)=q(a)$. And since the goal is a mere proposition, it automatically respects all path constructors, so we are done. ∎

###### Lemma 6.10.3.

For any set $B$, precomposing with $q$ yields an equivalence

 $(A/R\to B)\;\simeq\;\Bigl{(}\mathchoice{\sum_{(f:A\to B)}\,}{\mathchoice{{% \textstyle\sum_{(f:A\to B)}}}{\sum_{(f:A\to B)}}{\sum_{(f:A\to B)}}{\sum_{(f:A% \to B)}}}{\mathchoice{{\textstyle\sum_{(f:A\to B)}}}{\sum_{(f:A\to B)}}{\sum_{% (f:A\to B)}}{\sum_{(f:A\to B)}}}{\mathchoice{{\textstyle\sum_{(f:A\to B)}}}{% \sum_{(f:A\to B)}}{\sum_{(f:A\to B)}}{\sum_{(f:A\to B)}}}\mathchoice{\prod_{(a% ,b:A)}\,}{\mathchoice{{\textstyle\prod_{(a,b:A)}}}{\prod_{(a,b:A)}}{\prod_{(a,% b:A)}}{\prod_{(a,b:A)}}}{\mathchoice{{\textstyle\prod_{(a,b:A)}}}{\prod_{(a,b:% A)}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}}{\mathchoice{{\textstyle\prod_{(a,b:A)}% }}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}}R(a,b)\to(f(a)=f(b))% \Bigr{)}.$
###### Proof.

The quasi-inverse  of $\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}\circ q$, going from right to left, is just the recursion principle for $A/R$. That is, given $f:A\to B$ such that $\mathchoice{\prod_{a,b:A}\,}{\mathchoice{{\textstyle\prod_{(a,b:A)}}}{\prod_{(% a,b:A)}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}}{\mathchoice{{\textstyle\prod_{(a,b% :A)}}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}}{\mathchoice{{% \textstyle\prod_{(a,b:A)}}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}% }R(a,b)\to(f(a)=f(b)),$ we define $\bar{f}:A/R\to B$ by $\bar{f}(q(a)):\!\!\equiv f(a)$. This defining equation says precisely that $(f\mapsto\bar{f})$ is a right inverse   to $(\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}\circ q)$.

For it to also be a left inverse, we must show that for any $g:A/R\to B$ and $x:A/R$ we have $g(x)=\overline{g\circ q}$. However, by Lemma 6.10.2 (http://planetmath.org/610quotients#Thmprelem1) there merely exists $a$ such that $q(a)=x$. Since our desired equality is a mere proposition, we may assume there purely exists such an $a$, in which case $g(x)=g(q(a))=\overline{g\circ q}(q(a))=\overline{g\circ q}(x)$. ∎

Of course, classically the usual case to consider is when $R$ is an , i.e. we have

• : $\mathchoice{\prod_{a:A}\,}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)% }}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod% _{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}% }{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}R(a,a)$,

• : $\mathchoice{\prod_{a,b:A}\,}{\mathchoice{{\textstyle\prod_{(a,b:A)}}}{\prod_{(% a,b:A)}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}}{\mathchoice{{\textstyle\prod_{(a,b% :A)}}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}}{\mathchoice{{% \textstyle\prod_{(a,b:A)}}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}% }R(a,b)\to R(b,a)$, and

• transitivity: $\mathchoice{\prod_{a,b,c:C}\,}{\mathchoice{{\textstyle\prod_{(a,b,c:C)}}}{% \prod_{(a,b,c:C)}}{\prod_{(a,b,c:C)}}{\prod_{(a,b,c:C)}}}{\mathchoice{{% \textstyle\prod_{(a,b,c:C)}}}{\prod_{(a,b,c:C)}}{\prod_{(a,b,c:C)}}{\prod_{(a,% b,c:C)}}}{\mathchoice{{\textstyle\prod_{(a,b,c:C)}}}{\prod_{(a,b,c:C)}}{\prod_% {(a,b,c:C)}}{\prod_{(a,b,c:C)}}}R(a,b)\times R(b,c)\to R(a,c)$.

In this case, the set-quotient $A/R$ has additional good properties, as we will see in §10.1 (http://planetmath.org/101thecategoryofsets): for instance, we have $R(a,b)\simeq(q(a)=_{A/R}q(b))$. We often write an equivalence relation $R(a,b)$ infix as $a\sim b$.

###### Definition 6.10.4.

A predicate  $P:A\to\mathsf{Prop}$ is an equivalence class of a relation $R:A\times A\to\mathsf{Prop}$ if there merely exists an $a:A$ such that for all $b:A$ we have $R(a,b)\simeq P(b)$.

As $R$ and $P$ are mere propositions, the equivalence $R(a,b)\simeq P(b)$ is the same thing as implications  $R(a,b)\to P(b)$ and $P(b)\to R(a,b)$. And of course, for any $a:A$ we have the canonical equivalence class $P_{a}(b):\!\!\equiv R(a,b)$.

###### Definition 6.10.5.

We define

 $A\sslash R:\!\!\equiv\setof{P:A\to\mathsf{Prop}|P\text{ is an equivalence % class of }R}.$

The function $q^{\prime}:A\to A\sslash R$ is defined by $q^{\prime}(a):\!\!\equiv P_{a}$.

###### Proof.

First, note that if $R(a,b)$, then since $R$ is an equivalence relation we have $R(a,c)\Leftrightarrow R(b,c)$ for any $c:A$. Thus, $R(a,c)=R(b,c)$ by univalence, hence $P_{a}=P_{b}$ by function extensionality, i.e. $q^{\prime}(a)=q^{\prime}(b)$. Therefore, by Lemma 6.10.3 (http://planetmath.org/610quotients#Thmprelem2) we have an induced map $f:A/R\to A\sslash R$ such that $f\circ q=q^{\prime}$.

We show that $f$ is injective  and surjective, hence an equivalence. Surjectivity follows immediately from the fact that $q^{\prime}$ is surjective, which in turn is true essentially by definition of $A\sslash R$. For injectivity, if $f(x)=f(y)$, then to show the mere proposition $x=y$, by surjectivity of $q$ we may assume $x=q(a)$ and $y=q(b)$ for some $a,b:A$. Then $R(a,c)=f(q(a))(c)=f(q(b))(c)=R(b,c)$ for any $c:A$, and in particular $R(a,b)=R(b,b)$. But $R(b,b)$ is inhabited, since $R$ is an equivalence relation, hence so is $R(a,b)$. Thus $q(a)=q(b)$ and so $x=y$. ∎

In §10.1.3 (http://planetmath.org/1013quotients) we will give an alternative proof of this theorem. Note that unlike $A/R$, the construction $A\sslash R$ raises universe  level: if $A:\mathcal{U}_{i}$ and $R:A\to A\to\mathsf{Prop}_{\mathcal{U}_{i}}$, then in the definition of $A\sslash R$ we must also use $\mathsf{Prop}_{\mathcal{U}_{i}}$ to include all the equivalence classes, so that $A\sslash R:\mathcal{U}_{i+1}$. Of course, we can avoid this if we assume the propositional resizing axiom from §3.5 (http://planetmath.org/35subsetsandpropositionalresizing).

###### Remark 6.10.7.

The previous two constructions provide quotients in generality, but in particular cases there may be easier constructions. For instance, we may define the integers $\mathbb{Z}$ as a set-quotient

 $\mathbb{Z}:\!\!\equiv(\mathbb{N}\times\mathbb{N})/{\sim}$

where $\sim$ is the equivalence relation defined by

 $(a,b)\sim(c,d):\!\!\equiv(a+d=b+c).$

In other words, a pair $(a,b)$ represents the integer $a-b$. In this case, however, there are canonical representatives of the equivalence classes: those of the form $(n,0)$ or $(0,n)$.

The following lemma says that when this sort of thing happens, we don’t need either general construction of quotients. (A function $r:A\to A$ is called if $r\circ r=r$.)

###### Lemma 6.10.8.

Suppose $\sim$ is an equivalence relation on a set $A$, and there exists an idempotent $r:A\to A$ such that, for all $x,y\in A$, $(r(x)=r(y))\simeq(x\sim y)$. Then the type

 $(A/{\sim}):\!\!\equiv\mathchoice{\sum_{x:A}\,}{\mathchoice{{\textstyle\sum_{(x% :A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_% {(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle% \sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}r(x)=x$

is the set-quotient of $A$ by $\sim$. In other words, there is a map $q:A\to(A/{\sim})$ such that for every set $B$, the type $(A/{\sim})\to B$ is equivalent to

 $\mathchoice{\sum_{(g:A\to B)}\,}{\mathchoice{{\textstyle\sum_{(g:A\to B)}}}{% \sum_{(g:A\to B)}}{\sum_{(g:A\to B)}}{\sum_{(g:A\to B)}}}{\mathchoice{{% \textstyle\sum_{(g:A\to B)}}}{\sum_{(g:A\to B)}}{\sum_{(g:A\to B)}}{\sum_{(g:A% \to B)}}}{\mathchoice{{\textstyle\sum_{(g:A\to B)}}}{\sum_{(g:A\to B)}}{\sum_{% (g:A\to B)}}{\sum_{(g:A\to B)}}}\mathchoice{\prod_{(x,y:A)}\,}{\mathchoice{{% \textstyle\prod_{(x,y:A)}}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}% }{\mathchoice{{\textstyle\prod_{(x,y:A)}}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}{% \prod_{(x,y:A)}}}{\mathchoice{{\textstyle\prod_{(x,y:A)}}}{\prod_{(x,y:A)}}{% \prod_{(x,y:A)}}{\prod_{(x,y:A)}}}(x\sim y)\to(g(x)=g(y))$ (6.10.8)

with the map being induced by precomposition with $q$.

###### Proof.

Let $i:\mathchoice{\prod_{x:A}\,}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:% A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{% \prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x% :A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}r(r(x))=r(x)$ witness idempotence of $r$. The map $q:A\to A/{\sim}$ is defined by $q(x):\!\!\equiv(r(x),i(x))$. An equivalence $e$ from $A/{\sim}\to B$ to (6.10.8) is defined by

 $e(f):\!\!\equiv(f\circ q,\mathord{\hskip 1.0pt\underline{\hskip 4.3pt}\hskip 1% .0pt}),$

where the underscore $\mathord{\hskip 1.0pt\underline{\hskip 4.3pt}\hskip 1.0pt}$ denotes the following proof: if $x,y:A$ and $x\sim y$ then by assumption  $r(x)=r(y)$, hence $(r(x),i(x))=(r(y),i(y))$ as $A$ is a set, therefore $f(q(x))=f(q(y))$. To see that $e$ is an equivalence, consider the map $e^{\prime}$ in the opposite direction,

 $e^{\prime}(g,p)(x,q)\equiv g(x).$

Given any $f:A/{\sim}\to B$,

 $e^{\prime}(e(f))(x,p)\equiv f(q(x))\equiv f(r(x),i(x))=f(x,p)$

where the last equality holds because $p:r(x)=x$ and so $(x,p)=(r(x),i(x))$ because $A$ is a set. Similarly we compute

 $e(e^{\prime}(g,p))\equiv e(g\circ\mathsf{pr}_{1})\equiv(f\circ\mathsf{pr}_{1}% \circ q,{\mathord{\hskip 1.0pt\underline{\hskip 4.3pt}\hskip 1.0pt}}).$

Because $B$ is a set we need not worry about the $\mathord{\hskip 1.0pt\underline{\hskip 4.3pt}\hskip 1.0pt}$ part, while for the first component we have

 $f(\mathsf{pr}_{1}(q(x))):\!\!\equiv f(r(x))=f(x),$

where the last equation holds because $r(x)\sim x$ and $f$ respects $\sim$ by assumption. ∎

###### Corollary 6.10.10.

Suppose $p:A\to B$ is a retraction between sets. Then $B$ is the quotient of $A$ by the equivalence relation $\sim$ defined by

 $(a_{1}\sim a_{2}):\!\!\equiv(p(a_{1})=p(a_{2})).$
###### Remark 6.10.11.

Lemma 6.10.8 (http://planetmath.org/610quotients#Thmprelem3) applies to $\mathbb{Z}$ with the idempotent $r:\mathbb{N}\times\mathbb{N}\to\mathbb{N}\times\mathbb{N}$ defined by

 $r(a,b)=\begin{cases}(a-b,0)&\text{if a\geq b,}\\ (0,b-a)&\text{otherwise.}\end{cases}$

(This is a valid definition even constructively, since the relation $\geq$ on $\mathbb{N}$ is decidable.) Thus a non-negative integer is canonically represented as $(k,0)$ and a non-positive one by $(0,m)$, for $k,m:\mathbb{N}$. This division into cases implies the following induction principle for integers, which will be useful in http://planetmath.org/node/87582Chapter 8. (As usual, we identify natural numbers  with the corresponding non-negative integers.)

###### Lemma 6.10.12.

Suppose $P:\mathbb{Z}\to\mathcal{U}$ is a type family and that we have

• $d_{0}:P(0)$,

• $d_{+}:\mathchoice{\prod_{n:\mathbb{N}}\,}{\mathchoice{{\textstyle\prod_{(n:% \mathbb{N})}}}{\prod_{(n:\mathbb{N})}}{\prod_{(n:\mathbb{N})}}{\prod_{(n:% \mathbb{N})}}}{\mathchoice{{\textstyle\prod_{(n:\mathbb{N})}}}{\prod_{(n:% \mathbb{N})}}{\prod_{(n:\mathbb{N})}}{\prod_{(n:\mathbb{N})}}}{\mathchoice{{% \textstyle\prod_{(n:\mathbb{N})}}}{\prod_{(n:\mathbb{N})}}{\prod_{(n:\mathbb{N% })}}{\prod_{(n:\mathbb{N})}}}P(n)\to P(\mathsf{succ}(n))$, and

• $d_{-}:\mathchoice{\prod_{n:\mathbb{N}}\,}{\mathchoice{{\textstyle\prod_{(n:% \mathbb{N})}}}{\prod_{(n:\mathbb{N})}}{\prod_{(n:\mathbb{N})}}{\prod_{(n:% \mathbb{N})}}}{\mathchoice{{\textstyle\prod_{(n:\mathbb{N})}}}{\prod_{(n:% \mathbb{N})}}{\prod_{(n:\mathbb{N})}}{\prod_{(n:\mathbb{N})}}}{\mathchoice{{% \textstyle\prod_{(n:\mathbb{N})}}}{\prod_{(n:\mathbb{N})}}{\prod_{(n:\mathbb{N% })}}{\prod_{(n:\mathbb{N})}}}P(-n)\to P(-\mathsf{succ}(n))$.

Then we have $f:\mathchoice{\prod_{z:\mathbb{Z}}\,}{\mathchoice{{\textstyle\prod_{(z:\mathbb% {Z})}}}{\prod_{(z:\mathbb{Z})}}{\prod_{(z:\mathbb{Z})}}{\prod_{(z:\mathbb{Z})}% }}{\mathchoice{{\textstyle\prod_{(z:\mathbb{Z})}}}{\prod_{(z:\mathbb{Z})}}{% \prod_{(z:\mathbb{Z})}}{\prod_{(z:\mathbb{Z})}}}{\mathchoice{{\textstyle\prod_% {(z:\mathbb{Z})}}}{\prod_{(z:\mathbb{Z})}}{\prod_{(z:\mathbb{Z})}}{\prod_{(z:% \mathbb{Z})}}}P(z)$ such that $f(0)\equiv d_{0}$ and $f(\mathsf{succ}(n))\equiv d_{+}(f(n))$, and $f(-\mathsf{succ}(n))\equiv d_{-}(f(-n))$ for all $n:\mathbb{N}$.

###### Proof.

We identify $\mathbb{Z}$ with $\mathchoice{\sum_{x:\mathbb{N}\times\mathbb{N}}\,}{\mathchoice{{\textstyle\sum% _{(x:\mathbb{N}\times\mathbb{N})}}}{\sum_{(x:\mathbb{N}\times\mathbb{N})}}{% \sum_{(x:\mathbb{N}\times\mathbb{N})}}{\sum_{(x:\mathbb{N}\times\mathbb{N})}}}% {\mathchoice{{\textstyle\sum_{(x:\mathbb{N}\times\mathbb{N})}}}{\sum_{(x:% \mathbb{N}\times\mathbb{N})}}{\sum_{(x:\mathbb{N}\times\mathbb{N})}}{\sum_{(x:% \mathbb{N}\times\mathbb{N})}}}{\mathchoice{{\textstyle\sum_{(x:\mathbb{N}% \times\mathbb{N})}}}{\sum_{(x:\mathbb{N}\times\mathbb{N})}}{\sum_{(x:\mathbb{N% }\times\mathbb{N})}}{\sum_{(x:\mathbb{N}\times\mathbb{N})}}}(r(x)=x)$, where $r$ is the above idempotent. Now define $Q:\!\!\equiv P\circ r:\mathbb{N}\times\mathbb{N}\to\mathcal{U}$. We can construct $g:\mathchoice{\prod_{x:\mathbb{N}\times\mathbb{N}}\,}{\mathchoice{{\textstyle% \prod_{(x:\mathbb{N}\times\mathbb{N})}}}{\prod_{(x:\mathbb{N}\times\mathbb{N})% }}{\prod_{(x:\mathbb{N}\times\mathbb{N})}}{\prod_{(x:\mathbb{N}\times\mathbb{N% })}}}{\mathchoice{{\textstyle\prod_{(x:\mathbb{N}\times\mathbb{N})}}}{\prod_{(% x:\mathbb{N}\times\mathbb{N})}}{\prod_{(x:\mathbb{N}\times\mathbb{N})}}{\prod_% {(x:\mathbb{N}\times\mathbb{N})}}}{\mathchoice{{\textstyle\prod_{(x:\mathbb{N}% \times\mathbb{N})}}}{\prod_{(x:\mathbb{N}\times\mathbb{N})}}{\prod_{(x:\mathbb% {N}\times\mathbb{N})}}{\prod_{(x:\mathbb{N}\times\mathbb{N})}}}Q(x)$ by double induction on $n$:

 $\displaystyle g(0,0)$ $\displaystyle:\!\!\equiv d_{0},$ $\displaystyle g(\mathsf{succ}(n),0)$ $\displaystyle:\!\!\equiv d_{+}(g(n,0)),$ $\displaystyle g(0,\mathsf{succ}(m))$ $\displaystyle:\!\!\equiv d_{-}(g(0,m)),$ $\displaystyle g(\mathsf{succ}(n),\mathsf{succ}(m))$ $\displaystyle:\!\!\equiv g(n,m).$

Let $f$ be the restriction    of $g$ to $\mathbb{Z}$. ∎

For example, we can define the $n$-fold concatenation  of a loop for any integer $n$.

###### Corollary 6.10.13.

Let $A$ be a type with $a:A$ and $p:a=a$. There is a function $\mathchoice{\prod_{n:\mathbb{Z}}\,}{\mathchoice{{\textstyle\prod_{(n:\mathbb{Z% })}}}{\prod_{(n:\mathbb{Z})}}{\prod_{(n:\mathbb{Z})}}{\prod_{(n:\mathbb{Z})}}}% {\mathchoice{{\textstyle\prod_{(n:\mathbb{Z})}}}{\prod_{(n:\mathbb{Z})}}{\prod% _{(n:\mathbb{Z})}}{\prod_{(n:\mathbb{Z})}}}{\mathchoice{{\textstyle\prod_{(n:% \mathbb{Z})}}}{\prod_{(n:\mathbb{Z})}}{\prod_{(n:\mathbb{Z})}}{\prod_{(n:% \mathbb{Z})}}}(a=a)$, denoted $n\mapsto p^{n}$, defined by

 $\displaystyle p^{0}$ $\displaystyle:\!\!\equiv\mathsf{refl}_{\mathsf{base}}$ $\displaystyle p^{n+1}$ $\displaystyle:\!\!\equiv p^{n}\mathchoice{\mathbin{\raisebox{2.15pt}{% \displaystyle\centerdot}}}{\mathbin{\raisebox{2.15pt}{\centerdot}}}{% \mathbin{\raisebox{1.075pt}{\scriptstyle\,\centerdot\,}}}{\mathbin{\raisebox% {0.43pt}{\scriptscriptstyle\,\centerdot\,}}}p$ for $n\geq 0$ $\displaystyle p^{n-1}$ $\displaystyle:\!\!\equiv p^{n}\mathchoice{\mathbin{\raisebox{2.15pt}{% \displaystyle\centerdot}}}{\mathbin{\raisebox{2.15pt}{\centerdot}}}{% \mathbin{\raisebox{1.075pt}{\scriptstyle\,\centerdot\,}}}{\mathbin{\raisebox% {0.43pt}{\scriptscriptstyle\,\centerdot\,}}}\mathord{{p}^{-1}}$ for $n\leq 0$.

We will discuss the integers further in §6.11 (http://planetmath.org/611algebra),§11.1 (http://planetmath.org/111thefieldofrationalnumbers).

Title 6.10 Quotients
\metatable