Now that we know that is regular, to show that is exact, we need to show that every equivalence relation is effective. In other words, given an equivalence relation , there is a coequalizer of the pair and, moreover, the and form the kernel pair of .
We have already seen, in \autorefsec:set-quotients, two general ways to construct the quotient of a set by an equivalence relation . The first can be described as the set-coequalizer of the two projections
The important property of such a quotient is the following.
Suppose is an equivalence relation. Then there is an equivalence
for any . In other words, equivalence relations are effective.
We begin by extending to a relation , which we will then show is equivalent to the identity type on . We define by double induction on (note that is a set by univalence for mere propositions). We define . For and , the transitivity and symmetry of gives an equivalence from to . This completes the definition of .
It remains to show that for every . The direction follows by transport once we show that is reflexive, which is an easy induction. The other direction is a mere proposition, so since is surjective, it suffices to assume that and are of the form and . But in this case, we have the canonical map . (Note again the appearance of the encode-decode method.) ∎
This requires propositional resizing in order to remain in the same universe as and .
Note that if we regard as a function from to , then is equivalent to , 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.
For any function between any two sets, the relation given by is effective.
We will use that is the coequalizer of . Note that the kernel pair of the function
consists of the two projections
For any , we have equivalences
where the last equivalence holds because is a mere proposition for any . Therefore, we get that
and hence we may conclude that is an effective relation for any function . ∎
Equivalence relations are effective and there is an equivalence .
We need to analyze the coequalizer diagram
By the univalence axiom, the type is equivalent to the type of homotopies from to , which is equivalent to Since is an equivalence relation, the latter space is equivalent to . To summarize, we get that , so 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 . ∎
We finish this section by mentioning a possible third construction of the quotient of a set by an equivalence relation . Consider the precategory with objects and hom-sets ; 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.