10.1.3 Quotients

Now that we know that ๐’ฎโขeโขt is regular, to show that ๐’ฎโขeโขt is exact, we need to show that every equivalence relationMathworldPlanetmath is effective. In other words, given an equivalence relation R:Aโ†’Aโ†’๐–ฏ๐—‹๐—ˆ๐—‰, there is a coequalizerMathworldPlanetmath cR of the pair ๐—‰๐—‹1,๐—‰๐—‹2:โˆ‘(x,y:A)Rโข(x,y)โ†’A and, moreover, the ๐—‰๐—‹1 and ๐—‰๐—‹2 form the kernel pair of cR.

We have already seen, in \autorefsec:set-quotients, two general ways to construct the quotient of a set by an equivalence relation R:Aโ†’Aโ†’๐–ฏ๐—‹๐—ˆ๐—‰. The first can be described as the set-coequalizer of the two projections


The important property of such a quotient is the following.

Definition 10.1.1.

A relationMathworldPlanetmathPlanetmath R:Aโ†’Aโ†’Prop is said to be effective if the square


is a pullbackPlanetmathPlanetmath.

Since the standard pullback of cR and itself is โˆ‘(x,y:A)(cR(x)=cR(y)), by \autorefthm:total-fiber-equiv this is equivalentMathworldPlanetmathPlanetmathPlanetmath to asking that the canonical transformation โˆ(x,y:A)R(x,y)โ†’(cR(x)=cR(y)) be a fiberwise equivalence.

Lemma 10.1.2.

Suppose (A,R) is an equivalence relation. Then there is an equivalence


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


We begin by extending R to a relation R~:A/Rโ†’A/Rโ†’๐–ฏ๐—‹๐—ˆ๐—‰, which we will then show is equivalent to the identity type on A/R. We define R~ by double inductionMathworldPlanetmath on A/R (note that ๐–ฏ๐—‹๐—ˆ๐—‰ is a set by univalence for mere propositions). We define R~(cR(x),cR(y)):โ‰กR(x,y). For r:Rโข(x,xโ€ฒ) and s:Rโข(y,yโ€ฒ), the transitivity and symmetryPlanetmathPlanetmath of R gives an equivalence from Rโข(x,y) to Rโข(xโ€ฒ,yโ€ฒ). This completesPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath the definition of R~.

It remains to show that R~(w,wโ€ฒ)โ‰ƒ(w=wโ€ฒ) for every w,wโ€ฒ:A/R. The direction (w=wโ€ฒ)โ†’R~(w,wโ€ฒ) follows by transport once we show that R~ is reflexiveMathworldPlanetmathPlanetmath, which is an easy induction. The other direction R~(w,wโ€ฒ)โ†’(w=wโ€ฒ) is a mere proposition, so since cR:Aโ†’A/R is surjectivePlanetmathPlanetmath, it suffices to assume that w and wโ€ฒ are of the form cRโข(x) and cRโข(y). But in this case, we have the canonical map R~(cR(x),cR(y)):โ‰กR(x,y)โ†’(cR(x)=cR(y)). (Note again the appearance of the encode-decode method.) โˆŽ

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

A\sslashR:โ‰ก\setofP:Aโ†’๐–ฏ๐—‹๐—ˆ๐—‰|Pย is an equivalence class ofย R

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

Note that if we regard R as a function from A to Aโ†’๐–ฏ๐—‹๐—ˆ๐—‰, then Aโข\sslashโขR is equivalent to ๐—‚๐—†โข(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


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โ†’B between any two sets, the relation kerโก(f):Aโ†’Aโ†’Prop given by ker(f,x,y):โ‰ก(f(x)=f(y)) is effective.


We will use that ๐—‚๐—†โข(f) is the coequalizer of ๐—‰๐—‹1,๐—‰๐—‹2:(โˆ‘(x,y:A)f(x)=f(y))โ†’A. Note that the kernel pair of the function


consists of the two projections


For any x,y:A, we have equivalences

(cfโข(x)=cfโข(y)) โ‰ƒ(โˆ‘p:fโข(x)=fโข(y)p*(โˆฅ(x,๐—‹๐–พ๐–ฟ๐—…fโข(x))โˆฅ)=โˆฅ(y,๐—‹๐–พ๐–ฟ๐—…fโข(x))โˆฅ)

where the last equivalence holds because โˆฅ๐–ฟ๐—‚๐–ปfโข(b)โˆฅ is a mere proposition for any b:B. Therefore, we get that


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โ‰ƒAโข\sslashโขR.


We need to analyze the coequalizer diagram


By the univalence axiom, the type Rโข(x)=Rโข(y) is equivalent to the type of homotopiesMathworldPlanetmath from Rโข(x) to Rโข(y), which is equivalent to โˆ(z:A)Rโข(x,z)โ‰ƒ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))โ‰ƒ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โ‰ƒAโข\sslashโขR. โˆŽ

We finish this sectionPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath 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