10.1.3 Quotients

Now that we know that $𝒮et$ is regular, to show that $𝒮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 \mathrm{𝖯𝗋𝗈𝗉}$, there is a coequalizer $c_R$ of the pair ${\mathrm{𝗉𝗋}}_1,{\mathrm{𝗉𝗋}}_2:{\sum }_{(x,y:A)}R(x,y)\to A$ and, moreover, the ${\mathrm{𝗉𝗋}}_1$ and ${\mathrm{𝗉𝗋}}_2$ form the kernel pair of $c_R$.

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

$${\mathrm{𝗉𝗋}}_1,{\mathrm{𝗉𝗋}}_2:\left(\sum _{x,y:A}R(x,y)\right)\to A.$$

The important property of such a quotient is the following.

Definition 10.1.1.

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

is a pullback.

Since the standard pullback of $c_R$ and itself is ${\sum }_{(x,y:A)}(c_R(x)=c_R(y))$, by thm:total-fiber-equiv this is equivalent to asking that the canonical transformation ${\prod }_{(x,y:A)}R(x,y)\to (c_R(x)=c_R(y))$ be a fiberwise equivalence.

Lemma 10.1.2.

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

$$(c_R(x)=c_R(y))\simeq R(x,y)$$

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

Proof.

We begin by extending $R$ to a relation $\tilde{R}:A/R\to A/R\to \mathrm{𝖯𝗋𝗈𝗉}$, which we will then show is equivalent to the identity type on $A/R$. We define $\tilde{R}$ by double induction on $A/R$ (note that $\mathrm{𝖯𝗋𝗈𝗉}$ is a set by univalence for mere propositions). We define $\tilde{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 $\tilde{R}$.

It remains to show that $\tilde{R}(w,w^{\prime })\simeq (w=w^{\prime })$ for every $w,w^{\prime }:A/R$. The direction $(w=w^{\prime })\to \tilde{R}(w,w^{\prime })$ follows by transport once we show that $\tilde{R}$ is reflexive, which is an easy induction. The other direction $\tilde{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 $\tilde{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):

$$AR:\equiv P:A\to \mathrm{𝖯𝗋𝗈𝗉}|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 \mathrm{𝖯𝗋𝗈𝗉}$, then $AR$ is equivalent to $\mathrm{𝗂𝗆}(R)$, as constructed in sec:image. Now in lem:images_are_coequalizers we have shown that images are coequalizers. In particular, we immediately get the coequalizer diagram

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\mathrm{:}A\mathrm{\to }B$ between any two sets, the relation $\ker \mathit{}\mathrm{(}f\mathrm{)}\mathrm{:}A\mathrm{\to }A\mathrm{\to }\mathrm{Prop}$ given by $\ker \mathrm{(}f\mathrm{,}x\mathrm{,}y\mathrm{)}\mathrm{:}\mathrm{\equiv }\mathrm{(}f\mathrm{(}x\mathrm{)}\mathrm{=}f\mathrm{(}y\mathrm{)}\mathrm{)}$ is effective.

Proof.

We will use that $\mathrm{𝗂𝗆}(f)$ is the coequalizer of ${\mathrm{𝗉𝗋}}_1,{\mathrm{𝗉𝗋}}_2:({\sum }_{(x,y:A)}f(x)=f(y))\to A$. Note that the kernel pair of the function

$$c_f:\equiv \lambda a.(f(a),\parallel (a,{\mathrm{𝗋𝖾𝖿𝗅}}_{f(a)})\parallel ):A\to \mathrm{𝗂𝗆}(f)$$

consists of the two projections

$${\mathrm{𝗉𝗋}}_1,{\mathrm{𝗉𝗋}}_2:(\sum _{x,y:A}{c}_f(x)=c_f(y))\to A.$$

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

$(c_f(x)=c_f(y))$ $\simeq ({\displaystyle \sum _{p:f(x)=f(y)}}{p}_{*}\left(\parallel (x,{\mathrm{𝗋𝖾𝖿𝗅}}_{f(x)})\parallel \right)=\parallel (y,{\mathrm{𝗋𝖾𝖿𝗅}}_{f(x)})\parallel )$

$\simeq (f(x)=f(y)),$

where the last equivalence holds because $\parallel {\mathrm{𝖿𝗂𝖻}}_f(b)\parallel$ is a mere proposition for any $b:B$. Therefore, we get that

$$(\sum _{x,y:A}{c}_f(x)=c_f(y))\simeq (\sum _{x,y:A}f(x)=f(y))$$

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\mathrm{/}R\mathrm{\simeq }A\mathit{}\mathit{}R$.

Proof.

We need to analyze the coequalizer diagram

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 ${\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

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

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 sec:rezk) of this precategory will then be the quotient. The reader is invited to check the details.

Title	10.1.3 Quotients