6.10 Quotients

A particularly important sort of colimit of sets is the quotientPlanetmathPlanetmath by a relationMathworldPlanetmathPlanetmath. That is, let A be a set and R:AΓ—Aβ†’π–―π—‹π—ˆπ—‰ a family of mere propositions (a mere relation). Its quotient should be the set-coequalizer of the two projectionsPlanetmathPlanetmath


We can also describe this directly, as the higher inductive type A/R generated by

  • β€’

    A function q:A→A/R;

  • β€’

    For each a,b:A such that R⁒(a,b), an equality q⁒(a)=q⁒(b); and

  • β€’

    The 0-truncation constructor: for all x,y:A/R and r,s:x=y, we have r=s.

We may sometimes refer to A/R as the set-quotient of A by R, 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.)

Remark 6.10.1.

It is not actually necessary for the definition of set-quotients, and most of their properties, that A be a set. However, this is generally the case of most interest.

Lemma 6.10.2.

The function q:A→A/R is surjectivePlanetmathPlanetmath.


We must show that for any x:A/R there merely exists an a:A with q⁒(a)=x. We use the inductionMathworldPlanetmath principle of A/R. The first case is trivial: if x is q⁒(a), then of course there merely exists an a such that q⁒(a)=q⁒(a). And since the goal is a mere proposition, it automatically respects all path constructors, so we are done. ∎

Lemma 6.10.3.

For any set B, precomposing with q yields an equivalence


The quasi-inversePlanetmathPlanetmath of β€“βˆ˜q, going from right to left, is just the recursion principle for A/R. That is, given f:Aβ†’B such that ∏(a,b:A)R(a,b)β†’(f(a)=f(b)), we define fΒ―:A/Rβ†’B by fΒ―(q(a)):≑f(a). This defining equation says precisely that (f↦fΒ―) is a right inverseMathworldPlanetmathPlanetmath to (β€“βˆ˜q).

For it to also be a left inverse, we must show that for any g:A/Rβ†’B and x:A/R we have g⁒(x)=g∘qΒ―. However, by Lemma 6.10.2 (http://planetmath.org/610quotients#Thmprelem1) there merely exists a such that q⁒(a)=x. Since our desired equality is a mere proposition, we may assume there purely exists such an a, in which case g⁒(x)=g⁒(q⁒(a))=g∘q¯⁒(q⁒(a))=g∘q¯⁒(x). ∎

Of course, classically the usual case to consider is when R is an equivalence relationMathworldPlanetmath, i.e.Β we have

  • β€’

    reflexivityMathworldPlanetmath: ∏(a:A)R⁒(a,a),

  • β€’

    symmetryMathworldPlanetmathPlanetmathPlanetmath: ∏(a,b:A)R⁒(a,b)β†’R⁒(b,a), and

  • β€’

    transitivity: ∏(a,b,c:C)R⁒(a,b)Γ—R⁒(b,c)β†’R⁒(a,c).

In this case, the set-quotient A/R has additional good properties, as we will see in Β§10.1 (http://planetmath.org/101thecategoryofsets): for instance, we have R(a,b)≃(q(a)=A/Rq(b)). We often write an equivalence relation R⁒(a,b) infix as a∼b.

The quotient by an equivalence relation can also be constructed in other ways. The set theoretic approach is to consider the set of equivalence classesMathworldPlanetmath, as a subset of the power setMathworldPlanetmath of A. We can mimic this β€œimpredicative” construction in type theoryPlanetmathPlanetmath as well.

Definition 6.10.4.

A predicateMathworldPlanetmath P:Aβ†’Prop is an equivalence class of a relation R:AΓ—Aβ†’Prop if there merely exists an a:A such that for all b:A we have R⁒(a,b)≃P⁒(b).

As R and P are mere propositions, the equivalence R⁒(a,b)≃P⁒(b) is the same thing as implicationsMathworldPlanetmath R⁒(a,b)β†’P⁒(b) and P⁒(b)β†’R⁒(a,b). And of course, for any a:A we have the canonical equivalence class Pa(b):≑R(a,b).

Definition 6.10.5.

We define

Aβ«½R:≑\setofP:Aβ†’π–―π—‹π—ˆπ—‰|PΒ is an equivalence class ofΒ R.

The function qβ€²:Aβ†’Aβ«½R is defined by qβ€²(a):≑Pa.

Theorem 6.10.6.

For any equivalence relation R on A, the two set-quotients A/R and Aβ«½R are equivalentMathworldPlanetmathPlanetmathPlanetmath.


First, note that if R⁒(a,b), then since R is an equivalence relation we have R⁒(a,c)⇔R⁒(b,c) for any c:A. Thus, R⁒(a,c)=R⁒(b,c) by univalence, hence Pa=Pb by function extensionality, i.e.Β q′⁒(a)=q′⁒(b). Therefore, by Lemma 6.10.3 (http://planetmath.org/610quotients#Thmprelem2) we have an induced map f:A/Rβ†’Aβ«½R such that f∘q=qβ€².

We show that f is injectivePlanetmathPlanetmath and surjective, hence an equivalence. Surjectivity follows immediately from the fact that qβ€² is surjective, which in turn is true essentially by definition of Aβ«½R. For injectivity, if f⁒(x)=f⁒(y), then to show the mere proposition x=y, by surjectivity of q we may assume x=q⁒(a) and y=q⁒(b) for some a,b:A. Then R⁒(a,c)=f⁒(q⁒(a))⁒(c)=f⁒(q⁒(b))⁒(c)=R⁒(b,c) for any c:A, and in particular R⁒(a,b)=R⁒(b,b). But R⁒(b,b) is inhabited, since R is an equivalence relation, hence so is R⁒(a,b). Thus q⁒(a)=q⁒(b) and so x=y. ∎

In Β§10.1.3 (http://planetmath.org/1013quotients) we will give an alternative proof of this theorem. Note that unlike A/R, the construction Aβ«½R raises universePlanetmathPlanetmath level: if A:𝒰i and R:Aβ†’Aβ†’π–―π—‹π—ˆπ—‰π’°i, then in the definition of Aβ«½R we must also use π–―π—‹π—ˆπ—‰π’°i to include all the equivalence classes, so that Aβ«½R:𝒰i+1. Of course, we can avoid this if we assume the propositional resizing axiom from Β§3.5 (http://planetmath.org/35subsetsandpropositionalresizing).

Remark 6.10.7.

The previous two constructions provide quotients in generality, but in particular cases there may be easier constructions. For instance, we may define the integers Z as a set-quotient


where ∼ is the equivalence relation defined by


In other words, a pair (a,b) represents the integer a-b. In this case, however, there are canonical representatives of the equivalence classes: those of the form (n,0) or (0,n).

The following lemma says that when this sort of thing happens, we don’t need either general construction of quotients. (A function r:Aβ†’A is called idempotentMathworldPlanetmathPlanetmath if r∘r=r.)

Lemma 6.10.8.

Suppose ∼ is an equivalence relation on a set A, and there exists an idempotent r:Aβ†’A such that, for all x,y∈A, (r(x)=r(y))≃(x∼y). Then the type


is the set-quotient of A by ∼. In other words, there is a map q:Aβ†’(A/∼) such that for every set B, the type (A/∼)β†’B is equivalent to

βˆ‘(g:Aβ†’B)∏(x,y:A)(x∼y)β†’(g(x)=g(y)) (6.10.8)

with the map being induced by precomposition with q.


Let i:∏(x:A)r⁒(r⁒(x))=r⁒(x) witness idempotence ofΒ r. The map q:Aβ†’A/∼ is defined by q(x):≑(r(x),i(x)). An equivalence e from A/βˆΌβ†’B toΒ (6.10.8) is defined by


where the underscore Β― denotes the following proof: if x,y:A and x∼y then by assumptionPlanetmathPlanetmath r⁒(x)=r⁒(y), hence (r⁒(x),i⁒(x))=(r⁒(y),i⁒(y)) as A is a set, therefore f⁒(q⁒(x))=f⁒(q⁒(y)). To see that e is an equivalence, consider the map eβ€² in the opposite direction,


Given any f:A/βˆΌβ†’B,


where the last equality holds because p:r⁒(x)=x and so (x,p)=(r⁒(x),i⁒(x)) because A is a set. Similarly we compute


Because B is a set we need not worry about the Β― part, while for the first component we have


where the last equation holds because r⁒(x)∼x and f respects ∼ by assumption. ∎

Corollary 6.10.10.

Suppose p:Aβ†’B is a retraction between sets. Then B is the quotient of A by the equivalence relation ∼ defined by


Suppose s:Bβ†’A is a sectionMathworldPlanetmathPlanetmath of p. Then s∘p:Aβ†’A is an idempotent which satisfies the condition of Lemma 6.10.8 (http://planetmath.org/610quotients#Thmprelem3) for this ∼, and s induces an isomorphismPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath from B to its set of fixed points. ∎

Remark 6.10.11.

Lemma 6.10.8 (http://planetmath.org/610quotients#Thmprelem3) applies to Z with the idempotent r:N×N→N×N defined by

r⁒(a,b)={(a-b,0)ifΒ aβ‰₯b,(0,b-a)otherwise.

(This is a valid definition even constructively, since the relation β‰₯ on N is decidable.) Thus a non-negative integer is canonically represented as (k,0) and a non-positive one by (0,m), for k,m:N. 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 numbersMathworldPlanetmath with the corresponding non-negative integers.)

Lemma 6.10.12.

Suppose P:Z→U is a type family and that we have

  • β€’


  • β€’

    d+:∏(n:β„•)P⁒(n)β†’P⁒(π—Œπ—Žπ–Όπ–Όβ’(n)), and

  • β€’


Then we have f:∏(z:Z)P⁒(z) such that f⁒(0)≑d0 and f⁒(succ⁒(n))≑d+⁒(f⁒(n)), and f⁒(-succ⁒(n))≑d-⁒(f⁒(-n)) for all n:N.


We identify β„€ with βˆ‘(x:β„•Γ—β„•)(r(x)=x), where r is the above idempotent. Now define Q:≑P∘r:ℕ×ℕ→𝒰. We can construct g:∏(x:β„•Γ—β„•)Q⁒(x) by double induction on n:

g⁒(0,0) :≑d0,
g⁒(π—Œπ—Žπ–Όπ–Όβ’(n),0) :≑d+(g(n,0)),
g⁒(0,π—Œπ—Žπ–Όπ–Όβ’(m)) :≑d-(g(0,m)),
g⁒(π—Œπ—Žπ–Όπ–Όβ’(n),π—Œπ—Žπ–Όπ–Όβ’(m)) :≑g(n,m).

Let f be the restrictionPlanetmathPlanetmathPlanetmathPlanetmath of g to β„€. ∎

For example, we can define the n-fold concatenationMathworldPlanetmath of a loop for any integer n.

Corollary 6.10.13.

Let A be a type with a:A and p:a=a. There is a function ∏(n:Z)(a=a), denoted n↦pn, defined by

p0 :β‰‘π—‹π–Ύπ–Ώπ—…π–»π–Ίπ—Œπ–Ύ
pn+1 :≑pn\centerdotp for nβ‰₯0
pn-1 :≑pn\centerdotp-1 for n≀0.

We will discuss the integers further in Β§6.11 (http://planetmath.org/611algebra),Β§11.1 (http://planetmath.org/111thefieldofrationalnumbers).

Title 6.10 Quotients