# 10.1.3 Quotients

Now that we know that $\mathcal{S}et$ is regular, to show that $\mathcal{S}et$ is exact, we need to show that every equivalence relation is effective. In other words, given an equivalence relation $R:A\to A\to\mathsf{Prop}$, there is a coequalizer $c_{R}$ of the pair $\mathsf{pr}_{1},\mathsf{pr}_{2}:\mathchoice{\sum_{x,y:A}\,}{\mathchoice{{% \textstyle\sum_{(x,y:A)}}}{\sum_{(x,y:A)}}{\sum_{(x,y:A)}}{\sum_{(x,y:A)}}}{% \mathchoice{{\textstyle\sum_{(x,y:A)}}}{\sum_{(x,y:A)}}{\sum_{(x,y:A)}}{\sum_{% (x,y:A)}}}{\mathchoice{{\textstyle\sum_{(x,y:A)}}}{\sum_{(x,y:A)}}{\sum_{(x,y:% A)}}{\sum_{(x,y:A)}}}R(x,y)\to A$ and, moreover, the $\mathsf{pr}_{1}$ and $\mathsf{pr}_{2}$ form the kernel pair of $c_{R}$.

We have already seen, in \autorefsec:set-quotients, two general ways to construct the quotient of a set by an equivalence relation $R:A\to A\to\mathsf{Prop}$. The first can be described as the set-coequalizer of the two projections

 $\mathsf{pr}_{1},\mathsf{pr}_{2}:\Bigl{(}\mathchoice{\sum_{x,y:A}\,}{% \mathchoice{{\textstyle\sum_{(x,y:A)}}}{\sum_{(x,y:A)}}{\sum_{(x,y:A)}}{\sum_{% (x,y:A)}}}{\mathchoice{{\textstyle\sum_{(x,y:A)}}}{\sum_{(x,y:A)}}{\sum_{(x,y:% A)}}{\sum_{(x,y:A)}}}{\mathchoice{{\textstyle\sum_{(x,y:A)}}}{\sum_{(x,y:A)}}{% \sum_{(x,y:A)}}{\sum_{(x,y:A)}}}R(x,y)\Bigr{)}\to A.$

The important property of such a quotient is the following.

###### Definition 10.1.1.

A relation $R:A\to A\to\mathsf{Prop}$ is said to be effective if the square

 $\xymatrix{{\mathchoice{\sum_{x,y:A}\,}{\mathchoice{{\textstyle\sum_{(x,y:A)}}}% {\sum_{(x,y:A)}}{\sum_{(x,y:A)}}{\sum_{(x,y:A)}}}{\mathchoice{{\textstyle\sum_% {(x,y:A)}}}{\sum_{(x,y:A)}}{\sum_{(x,y:A)}}{\sum_{(x,y:A)}}}{\mathchoice{{% \textstyle\sum_{(x,y:A)}}}{\sum_{(x,y:A)}}{\sum_{(x,y:A)}}{\sum_{(x,y:A)}}}R(x% ,y)}\ar[r]^{(}0.7){\mathsf{pr}_{1}}\ar[d]_{\mathsf{pr}_{2}}&{A}\ar[d]^{c_{R}}% \\ {A}\ar[r]_{c_{R}}&{A/R}}$

is a pullback.

Since the standard pullback of $c_{R}$ and itself is $\mathchoice{\sum_{x,y:A}\,}{\mathchoice{{\textstyle\sum_{(x,y:A)}}}{\sum_{(x,y% :A)}}{\sum_{(x,y:A)}}{\sum_{(x,y:A)}}}{\mathchoice{{\textstyle\sum_{(x,y:A)}}}% {\sum_{(x,y:A)}}{\sum_{(x,y:A)}}{\sum_{(x,y:A)}}}{\mathchoice{{\textstyle\sum_% {(x,y:A)}}}{\sum_{(x,y:A)}}{\sum_{(x,y:A)}}{\sum_{(x,y:A)}}}(c_{R}(x)=c_{R}(y))$, by \autorefthm:total-fiber-equiv this is equivalent to asking that the canonical transformation $\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)}}% }R(x,y)\to(c_{R}(x)=c_{R}(y))$ be a fiberwise equivalence.

###### Lemma 10.1.2.

Suppose ${\mathopen{}(A,R)\mathclose{}}$ is an equivalence relation. Then there is an equivalence

 $(c_{R}(x)=c_{R}(y))\simeq R(x,y)$

for any $x,y:A$. In other words, equivalence relations are effective.

###### Proof.

We begin by extending $R$ to a relation $\widetilde{R}:A/R\to A/R\to\mathsf{Prop}$, which we will then show is equivalent to the identity type on $A/R$. We define $\widetilde{R}$ by double induction on $A/R$ (note that $\mathsf{Prop}$ is a set by univalence for mere propositions). We define $\widetilde{R}(c_{R}(x),c_{R}(y)):\!\!\equiv R(x,y)$. For $r:R(x,x^{\prime})$ and $s:R(y,y^{\prime})$, the transitivity and symmetry of $R$ gives an equivalence from $R(x,y)$ to $R(x^{\prime},y^{\prime})$. This completes the definition of $\widetilde{R}$.

It remains to show that $\widetilde{R}(w,w^{\prime})\simeq(w=w^{\prime})$ for every $w,w^{\prime}:A/R$. The direction $(w=w^{\prime})\to\widetilde{R}(w,w^{\prime})$ follows by transport once we show that $\widetilde{R}$ is reflexive, which is an easy induction. The other direction $\widetilde{R}(w,w^{\prime})\to(w=w^{\prime})$ is a mere proposition, so since $c_{R}:A\to A/R$ is surjective, it suffices to assume that $w$ and $w^{\prime}$ are of the form $c_{R}(x)$ and $c_{R}(y)$. But in this case, we have the canonical map $\widetilde{R}(c_{R}(x),c_{R}(y)):\!\!\equiv R(x,y)\to(c_{R}(x)=c_{R}(y))$. (Note again the appearance of the encode-decode method.) ∎

The second construction of quotients is as the set of equivalence classes of $R$ (a subset of its power set):

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

This requires propositional resizing in order to remain in the same universe as $A$ and $R$.

Note that if we regard $R$ as a function from $A$ to $A\to\mathsf{Prop}$, then $A\sslash R$ is equivalent to $\mathsf{im}(R)$, as constructed in \autorefsec:image. Now in \autoreflem:images_are_coequalizers we have shown that images are coequalizers. In particular, we immediately get the coequalizer diagram

 $\xymatrix{**[l]{\mathchoice{\sum_{x,y:A}\,}{\mathchoice{{\textstyle\sum_{(x,y:% A)}}}{\sum_{(x,y:A)}}{\sum_{(x,y:A)}}{\sum_{(x,y:A)}}}{\mathchoice{{\textstyle% \sum_{(x,y:A)}}}{\sum_{(x,y:A)}}{\sum_{(x,y:A)}}{\sum_{(x,y:A)}}}{\mathchoice{% {\textstyle\sum_{(x,y:A)}}}{\sum_{(x,y:A)}}{\sum_{(x,y:A)}}{\sum_{(x,y:A)}}}R(% x)=R(y)}\ar@<0.25em>[r]^{\mathsf{pr}_{1}}\ar@<-0.25em>[r]_{\mathsf{pr}_{2}}&{A% }\ar[r]&{A\sslash R.}}$

We can use this to give an alternative proof that any equivalence relation is effective and that the two definitions of quotients agree.

###### Theorem 10.1.3.

For any function $f:A\to B$ between any two sets, the relation $\ker(f):A\to A\to\mathsf{Prop}$ given by $\ker(f,x,y):\!\!\equiv(f(x)=f(y))$ is effective.

###### Proof.

We will use that $\mathsf{im}(f)$ is the coequalizer of $\mathsf{pr}_{1},\mathsf{pr}_{2}:(\mathchoice{\sum_{x,y:A}\,}{\mathchoice{{% \textstyle\sum_{(x,y:A)}}}{\sum_{(x,y:A)}}{\sum_{(x,y:A)}}{\sum_{(x,y:A)}}}{% \mathchoice{{\textstyle\sum_{(x,y:A)}}}{\sum_{(x,y:A)}}{\sum_{(x,y:A)}}{\sum_{% (x,y:A)}}}{\mathchoice{{\textstyle\sum_{(x,y:A)}}}{\sum_{(x,y:A)}}{\sum_{(x,y:% A)}}{\sum_{(x,y:A)}}}f(x)=f(y))\to A$. Note that the kernel pair of the function

 $c_{f}:\!\!\equiv{\lambda}a.\,\Bigl{(}f(a),\mathopen{}\left\|{\mathopen{}(a,% \mathsf{refl}_{f(a)})\mathclose{}}\right\|\mathclose{}\Bigr{)}:A\to\mathsf{im}% (f)$

consists of the two projections

 $\mathsf{pr}_{1},\mathsf{pr}_{2}:\Bigl{(}\mathchoice{\sum_{x,y:A}\,}{% \mathchoice{{\textstyle\sum_{(x,y:A)}}}{\sum_{(x,y:A)}}{\sum_{(x,y:A)}}{\sum_{% (x,y:A)}}}{\mathchoice{{\textstyle\sum_{(x,y:A)}}}{\sum_{(x,y:A)}}{\sum_{(x,y:% A)}}{\sum_{(x,y:A)}}}{\mathchoice{{\textstyle\sum_{(x,y:A)}}}{\sum_{(x,y:A)}}{% \sum_{(x,y:A)}}{\sum_{(x,y:A)}}}c_{f}(x)=c_{f}(y)\Bigr{)}\to A.$

For any $x,y:A$, we have equivalences

 $\displaystyle(c_{f}(x)=c_{f}(y))$ $\displaystyle\simeq\Bigl{(}\mathchoice{\sum_{p:f(x)=f(y)}\,}{\mathchoice{{% \textstyle\sum_{(p:f(x)=f(y))}}}{\sum_{(p:f(x)=f(y))}}{\sum_{(p:f(x)=f(y))}}{% \sum_{(p:f(x)=f(y))}}}{\mathchoice{{\textstyle\sum_{(p:f(x)=f(y))}}}{\sum_{(p:% f(x)=f(y))}}{\sum_{(p:f(x)=f(y))}}{\sum_{(p:f(x)=f(y))}}}{\mathchoice{{% \textstyle\sum_{(p:f(x)=f(y))}}}{\sum_{(p:f(x)=f(y))}}{\sum_{(p:f(x)=f(y))}}{% \sum_{(p:f(x)=f(y))}}}{p}_{*}\mathopen{}\left({\mathopen{}\left\|{\mathopen{}(% x,\mathsf{refl}_{f(x)})\mathclose{}}\right\|\mathclose{}}\right)\mathclose{}=% \mathopen{}\left\|{\mathopen{}(y,\mathsf{refl}_{f(x)})\mathclose{}}\right\|% \mathclose{}\Bigr{)}$ $\displaystyle\simeq(f(x)=f(y)),$

where the last equivalence holds because $\mathopen{}\left\|{\mathsf{fib}}_{f}(b)\right\|\mathclose{}$ is a mere proposition for any $b:B$. Therefore, we get that

 $\Bigl{(}\mathchoice{\sum_{x,y:A}\,}{\mathchoice{{\textstyle\sum_{(x,y:A)}}}{% \sum_{(x,y:A)}}{\sum_{(x,y:A)}}{\sum_{(x,y:A)}}}{\mathchoice{{\textstyle\sum_{% (x,y:A)}}}{\sum_{(x,y:A)}}{\sum_{(x,y:A)}}{\sum_{(x,y:A)}}}{\mathchoice{{% \textstyle\sum_{(x,y:A)}}}{\sum_{(x,y:A)}}{\sum_{(x,y:A)}}{\sum_{(x,y:A)}}}c_{% f}(x)=c_{f}(y)\Bigr{)}\simeq\Bigl{(}\mathchoice{\sum_{x,y:A}\,}{\mathchoice{{% \textstyle\sum_{(x,y:A)}}}{\sum_{(x,y:A)}}{\sum_{(x,y:A)}}{\sum_{(x,y:A)}}}{% \mathchoice{{\textstyle\sum_{(x,y:A)}}}{\sum_{(x,y:A)}}{\sum_{(x,y:A)}}{\sum_{% (x,y:A)}}}{\mathchoice{{\textstyle\sum_{(x,y:A)}}}{\sum_{(x,y:A)}}{\sum_{(x,y:% A)}}{\sum_{(x,y:A)}}}f(x)=f(y)\Bigr{)}$

and hence we may conclude that $\ker f$ is an effective relation for any function $f$. ∎

###### Theorem 10.1.4.

Equivalence relations are effective and there is an equivalence $A/R\simeq A\sslash R$.

###### Proof.

We need to analyze the coequalizer diagram

 $\xymatrix{**[l]{\mathchoice{\sum_{x,y:A}\,}{\mathchoice{{\textstyle\sum_{(x,y:% A)}}}{\sum_{(x,y:A)}}{\sum_{(x,y:A)}}{\sum_{(x,y:A)}}}{\mathchoice{{\textstyle% \sum_{(x,y:A)}}}{\sum_{(x,y:A)}}{\sum_{(x,y:A)}}{\sum_{(x,y:A)}}}{\mathchoice{% {\textstyle\sum_{(x,y:A)}}}{\sum_{(x,y:A)}}{\sum_{(x,y:A)}}{\sum_{(x,y:A)}}}R(% x)=R(y)}\ar@<0.25em>[r]^{\mathsf{pr}_{1}}\ar@<-0.25em>[r]_{\mathsf{pr}_{2}}&{A% }\ar[r]&{A\sslash R}}$

By the univalence axiom, the type $R(x)=R(y)$ is equivalent to the type of homotopies from $R(x)$ to $R(y)$, which is equivalent to $\mathchoice{\prod_{z:A}\,}{\mathchoice{{\textstyle\prod_{(z:A)}}}{\prod_{(z:A)% }}{\prod_{(z:A)}}{\prod_{(z:A)}}}{\mathchoice{{\textstyle\prod_{(z:A)}}}{\prod% _{(z:A)}}{\prod_{(z:A)}}{\prod_{(z:A)}}}{\mathchoice{{\textstyle\prod_{(z:A)}}% }{\prod_{(z:A)}}{\prod_{(z:A)}}{\prod_{(z:A)}}}R(x,z)\simeq R(y,z).$ Since $R$ is an equivalence relation, the latter space is equivalent to $R(x,y)$. To summarize, we get that $(R(x)=R(y))\simeq R(x,y)$, so $R$ is effective since it is equivalent to an effective relation. Also, the diagram

 $\xymatrix{**[l]{\mathchoice{\sum_{x,y:A}\,}{\mathchoice{{\textstyle\sum_{(x,y:% A)}}}{\sum_{(x,y:A)}}{\sum_{(x,y:A)}}{\sum_{(x,y:A)}}}{\mathchoice{{\textstyle% \sum_{(x,y:A)}}}{\sum_{(x,y:A)}}{\sum_{(x,y:A)}}{\sum_{(x,y:A)}}}{\mathchoice{% {\textstyle\sum_{(x,y:A)}}}{\sum_{(x,y:A)}}{\sum_{(x,y:A)}}{\sum_{(x,y:A)}}}R(% x,y)}\ar@<0.25em>[r]^{\mathsf{pr}_{1}}\ar@<-0.25em>[r]_{\mathsf{pr}_{2}}&{A}% \ar[r]&{A\sslash R.}}$

is a coequalizer diagram. Since coequalizers are unique up to equivalence, it follows that $A/R\simeq A\sslash R$. ∎

We finish this section by mentioning a possible third construction of the quotient of a set $A$ by an equivalence relation $R$. Consider the precategory with objects $A$ and hom-sets $R$; the type of objects of the Rezk completion (see \autorefsec:rezk) of this precategory will then be the quotient. The reader is invited to check the details.

Title 10.1.3 Quotients
\metatable