A particularly important sort of colimit of sets is the quotient by a relation. That is, let be a set and a family of mere propositions (a mere relation). Its quotient should be the set-coequalizer of the two projections
We can also describe this directly, as the higher inductive type generated by
A function ;
For each such that , an equality ; and
The -truncation constructor: for all and , we have .
We may sometimes refer to as the set-quotient of by , 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.)
It is not actually necessary for the definition of set-quotients, and most of their properties, that be a set. However, this is generally the case of most interest.
The function is surjective.
For any set , precomposing with yields an equivalence
For it to also be a left inverse, we must show that for any and we have . However, by Lemma 6.10.2 (http://planetmath.org/610quotients#Thmprelem1) there merely exists such that . Since our desired equality is a mere proposition, we may assume there purely exists such an , in which case . ∎
Of course, classically the usual case to consider is when is an equivalence relation, i.e. we have
In this case, the set-quotient has additional good properties, as we will see in §10.1 (http://planetmath.org/101thecategoryofsets): for instance, we have . We often write an equivalence relation infix as .
The quotient by an equivalence relation can also be constructed in other ways. The set theoretic approach is to consider the set of equivalence classes, as a subset of the power set of . We can mimic this “impredicative” construction in type theory as well.
A predicate is an equivalence class of a relation if there merely exists an such that for all we have .
As and are mere propositions, the equivalence is the same thing as implications and . And of course, for any we have the canonical equivalence class .
The function is defined by .
For any equivalence relation on , the two set-quotients and are equivalent.
First, note that if , then since is an equivalence relation we have for any . Thus, by univalence, hence by function extensionality, i.e. . Therefore, by Lemma 6.10.3 (http://planetmath.org/610quotients#Thmprelem2) we have an induced map such that .
We show that is injective and surjective, hence an equivalence. Surjectivity follows immediately from the fact that is surjective, which in turn is true essentially by definition of . For injectivity, if , then to show the mere proposition , by surjectivity of we may assume and for some . Then for any , and in particular . But is inhabited, since is an equivalence relation, hence so is . Thus and so . ∎
In §10.1.3 (http://planetmath.org/1013quotients) we will give an alternative proof of this theorem. Note that unlike , the construction raises universe level: if and , then in the definition of we must also use to include all the equivalence classes, so that . Of course, we can avoid this if we assume the propositional resizing axiom from §3.5 (http://planetmath.org/35subsetsandpropositionalresizing).
The previous two constructions provide quotients in generality, but in particular cases there may be easier constructions. For instance, we may define the integers as a set-quotient
where is the equivalence relation defined by
In other words, a pair represents the integer . In this case, however, there are canonical representatives of the equivalence classes: those of the form or .
The following lemma says that when this sort of thing happens, we don’t need either general construction of quotients. (A function is called idempotent if .)
Suppose is an equivalence relation on a set , and there exists an idempotent such that, for all , . Then the type
is the set-quotient of by . In other words, there is a map such that for every set , the type is equivalent to
with the map being induced by precomposition with .
Let witness idempotence of . The map is defined by . An equivalence from to (6.10.8) is defined by
where the underscore denotes the following proof: if and then by assumption , hence as is a set, therefore . To see that is an equivalence, consider the map in the opposite direction,
Given any ,
where the last equality holds because and so because is a set. Similarly we compute
Because is a set we need not worry about the part, while for the first component we have
where the last equation holds because and respects by assumption. ∎
Suppose is a retraction between sets. Then is the quotient of by the equivalence relation defined by
Lemma 6.10.8 (http://planetmath.org/610quotients#Thmprelem3) applies to with the idempotent defined by
(This is a valid definition even constructively, since the relation on is decidable.) Thus a non-negative integer is canonically represented as and a non-positive one by , for . 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.)
Suppose is a type family and that we have
Then we have such that and , and for all .
We identify with , where is the above idempotent. Now define . We can construct by double induction on :
Let be the restriction of to . ∎
For example, we can define the -fold concatenation of a loop for any integer .
Let be a type with and . There is a function , denoted , defined by
We will discuss the integers further in §6.11 (http://planetmath.org/611algebra),§11.1 (http://planetmath.org/111thefieldofrationalnumbers).