6.10 Quotients

A particularly important sort of colimit of sets is the quotient by a relation.That is, let $A$ be a set and $R:A\times A\to \mathrm{𝖯𝗋𝗈𝗉}$ a family of mere propositions (a mere relation).Its quotient should be the set-coequalizer of the two projections

$${\sum }_{(a,b:A)}R(a,b)A.$$

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

• A function $q:A\to 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\mathrm{:}A\mathrm{\to }A\mathrm{/}R$ is surjective.

Proof.

We must show that for any $x:A/R$ there merely exists an $a:A$ with $q(a)=x$.We use the induction 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

$$(A/R\to B)\simeq (\sum _{(f:A\to B)}\prod _{(a,b:A)}R(a,b)\to (f(a)=f(b))).$$

Proof.

The quasi-inverse of $\text{–}\circ q$, going from right to left, is just the recursion principle for $A/R$.That is, given $f:A\to B$ such that${\prod }_{(a,b:A)}R(a,b)\to (f(a)=f(b)),$ we define $\overline{f}:A/R\to B$ by $\overline{f}(q(a)):\equiv f(a)$.This defining equation says precisely that $(f\mapsto \overline{f})$ is a right inverse to $(\text{–}\circ q)$.

For it to also be a left inverse, we must show that for any $g:A/R\to B$ and $x:A/R$ we have $g(x)=\overline{g\circ 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))=\overline{g\circ q}(q(a))=\overline{g\circ q}(x)$.∎

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

• reflexivity: ${\prod }_{(a:A)}R(a,a)$,

• symmetry: ${\prod }_{(a,b:A)}R(a,b)\to R(b,a)$, and

• transitivity: ${\prod }_{(a,b,c:C)}R(a,b)\times R(b,c)\to 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)\simeq (q(a){=}_{A/R}q(b))$.We often write an equivalence relation $R(a,b)$ infix as $a\sim 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 classes, as a subset of the power set of $A$.We can mimic this “impredicative” construction in type theory as well.

Definition 6.10.4.

A predicate $P\mathrm{:}A\mathrm{\to }\mathrm{Prop}$ is an equivalence classof a relation $R\mathrm{:}A\mathrm{\times }A\mathrm{\to }\mathrm{Prop}$ if there merely exists an $a\mathrm{:}A$ such that for all $b\mathrm{:}A$ we have $R\mathit{}\mathrm{(}a\mathrm{,}b\mathrm{)}\mathrm{\simeq }P\mathit{}\mathrm{(}b\mathrm{)}$.

As $R$ and $P$ are mere propositions, the equivalence $R(a,b)\simeq P(b)$ is the same thing as implications $R(a,b)\to P(b)$ and $P(b)\to R(a,b)$.And of course, for any $a:A$ we have the canonical equivalence class $P_a(b):\equiv R(a,b)$.

Definition 6.10.5.

We define

$$A⫽R:\equiv P:A\to \mathrm{𝖯𝗋𝗈𝗉}|P\mathit{\text{ is an equivalence class of }}R.$$

The function $q^{\mathrm{\prime }}\mathrm{:}A\mathrm{\to }A\mathrm{⫽}R$ is defined by $q^{\mathrm{\prime }}\mathrm{(}a\mathrm{)}\mathrm{:}\mathrm{\equiv }{P}_a$.

Theorem 6.10.6.

For any equivalence relation $R$ on $A$, the two set-quotients $A\mathrm{/}R$ and $A\mathrm{⫽}R$ are equivalent.

Proof.

First, note that if $R(a,b)$, then since $R$ is an equivalence relation we have $R(a,c)\iff R(b,c)$ for any $c:A$.Thus, $R(a,c)=R(b,c)$ by univalence, hence $P_a=P_b$ by function extensionality, i.e. $q^{\prime }(a)=q^{\prime }(b)$.Therefore, by Lemma 6.10.3 (http://planetmath.org/610quotients#Thmprelem2) we have an induced map $f:A/R\to A⫽R$ such that $f\circ q=q^{\prime }$.

We show that $f$ is injective and surjective, hence an equivalence.Surjectivity follows immediately from the fact that $q^{\prime }$ 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 universe level: if $A:{𝒰}_i$ and $R:A\to A\to {\mathrm{𝖯𝗋𝗈𝗉}}_{{𝒰}_i}$, then in the definition of $A⫽R$ we must also use ${\mathrm{𝖯𝗋𝗈𝗉}}_{{𝒰}_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 $\mathrm{Z}$ as a set-quotient

$$\mathbb{Z}:\equiv (\mathbb{N}\times \mathbb{N})/\sim$$

where $\mathrm{\sim }$ is the equivalence relation defined by

$$(a,b)\sim (c,d):\equiv (a+d=b+c).$$

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

The following lemma says that when this sort of thing happens, we don’t need either general construction of quotients.(A function $r:A\to A$ is called idempotentif $r\circ r=r$.)

Lemma 6.10.8.

Suppose $\mathrm{\sim }$ is an equivalence relation on a set $A$, and there exists an idempotent $r\mathrm{:}A\mathrm{\to }A$ such that, for all $x\mathrm{,}y\mathrm{\in }A$, $\mathrm{(}r\mathrm{(}x\mathrm{)}\mathrm{=}r\mathrm{(}y\mathrm{)}\mathrm{)}\mathrm{\simeq }\mathrm{(}x\mathrm{\sim }y\mathrm{)}$. Then thetype

$$(A/\sim ):\equiv \sum _{x:A}r(x)=x$$

is the set-quotient of $A$ by $\mathrm{\sim }$.In other words, there is a map $q\mathrm{:}A\mathrm{\to }\mathrm{(}A\mathrm{/}\mathrm{\sim }\mathrm{)}$ such that for every set $B$, the type $\mathrm{(}A\mathrm{/}\mathrm{\sim }\mathrm{)}\mathrm{\to }B$ is equivalent to

$$\sum _{(g:A\to B)}\prod _{(x,y:A)}(x\sim y)\to (g(x)=g(y))$$(6.10.8)

with the map being induced by precomposition with $q$.

Proof.

Let $i:{\prod }_{(x:A)}r(r(x))=r(x)$ witness idempotence of $r$.The map $q:A\to A/\sim$ is defined by $q(x):\equiv (r(x),i(x))$. An equivalence $e$from $A/\sim \to B$ to (6.10.8) is defined by

$$e(f):\equiv (f\circ q,\underset{¯}{}),$$

where the underscore $\underset{¯}{}$ denotes the following proof: if $x,y:A$ and $x\sim y$ then by assumption$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^{\prime }$ in the oppositedirection,

$$e^{\prime }(g,p)(x,q)\equiv g(x).$$

Given any $f:A/\sim \to B$,

$$e^{\prime }(e(f))(x,p)\equiv f(q(x))\equiv f(r(x),i(x))=f(x,p)$$

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

$$e(e^{\prime }(g,p))\equiv e(g\circ {\mathrm{𝗉𝗋}}_1)\equiv (f\circ {\mathrm{𝗉𝗋}}_1\circ q,\underset{¯}{}).$$

Because $B$ is a set we need not worry about the $\underset{¯}{}$ part, while for the firstcomponent we have

$$f({\mathrm{𝗉𝗋}}_1(q(x))):\equiv f(r(x))=f(x),$$

where the last equation holds because $r(x)\sim x$ and $f$ respects $\sim$ byassumption.∎

Corollary 6.10.10.

Suppose $p\mathrm{:}A\mathrm{\to }B$ is a retraction between sets.Then $B$ is the quotient of $A$ by the equivalence relation $\mathrm{\sim }$ defined by

$$(a_1\sim a_2):\equiv (p(a_1)=p(a_2)).$$

Proof.

Suppose $s:B\to A$ is a section of $p$.Then $s\circ p:A\to A$ is an idempotent which satisfies the condition of Lemma 6.10.8 (http://planetmath.org/610quotients#Thmprelem3) for this $\sim$, and $s$ induces an isomorphism from $B$ to its set of fixed points.∎

Remark 6.10.11.

Lemma 6.10.8 (http://planetmath.org/610quotients#Thmprelem3) applies to $\mathrm{Z}$ with the idempotent $r\mathrm{:}\mathrm{N}\mathrm{\times }\mathrm{N}\mathrm{\to }\mathrm{N}\mathrm{\times }\mathrm{N}$defined by

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

Lemma 6.10.12.

Suppose $P\mathrm{:}\mathrm{Z}\mathrm{\to }\mathrm{U}$ is a type family and that we have

• $d_0:P(0)$,

• $d_{+}:{\prod }_{(n:\mathbb{N})}P(n)\to P(\mathrm{𝗌𝗎𝖼𝖼}(n))$, and

• $d_{-}:{\prod }_{(n:\mathbb{N})}P(-n)\to P(-\mathrm{𝗌𝗎𝖼𝖼}(n))$.

Then we have $f\mathrm{:}{\mathrm{\prod }}_{\mathrm{(}z\mathrm{:}\mathrm{Z}\mathrm{)}}P\mathit{}\mathrm{(}z\mathrm{)}$ such that $f\mathit{}\mathrm{(}\mathrm{0}\mathrm{)}\mathrm{\equiv }{d}_{\mathrm{0}}$ and $f\mathit{}\mathrm{(}\mathrm{succ}\mathit{}\mathrm{(}n\mathrm{)}\mathrm{)}\mathrm{\equiv }{d}_{\mathrm{+}}\mathit{}\mathrm{(}f\mathit{}\mathrm{(}n\mathrm{)}\mathrm{)}$, and $f\mathit{}\mathrm{(}\mathrm{-}\mathrm{succ}\mathit{}\mathrm{(}n\mathrm{)}\mathrm{)}\mathrm{\equiv }{d}_{\mathrm{-}}\mathit{}\mathrm{(}f\mathit{}\mathrm{(}\mathrm{-}n\mathrm{)}\mathrm{)}$ for all $n\mathrm{:}\mathrm{N}$.

Proof.

We identify $\mathbb{Z}$ with ${\sum }_{(x:\mathbb{N}\times \mathbb{N})}(r(x)=x)$, where $r$ is the above idempotent.Now define $Q:\equiv P\circ r:\mathbb{N}\times \mathbb{N}\to 𝒰$.We can construct $g:{\prod }_{(x:\mathbb{N}\times \mathbb{N})}Q(x)$ by double induction on $n$:

$g(0,0)$$:\equiv d_0,$

$g(\mathrm{𝗌𝗎𝖼𝖼}(n),0)$$:\equiv d_{+}(g(n,0)),$

$g(0,\mathrm{𝗌𝗎𝖼𝖼}(m))$$:\equiv d_{-}(g(0,m)),$

$g(\mathrm{𝗌𝗎𝖼𝖼}(n),\mathrm{𝗌𝗎𝖼𝖼}(m))$$:\equiv g(n,m).$

Let $f$ be the restriction of $g$ to $\mathbb{Z}$.∎

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

Corollary 6.10.13.

Let $A$ be a type with $a\mathrm{:}A$ and $p\mathrm{:}a\mathrm{=}a$.There is a function ${\mathrm{\prod }}_{\mathrm{(}n\mathrm{:}\mathrm{Z}\mathrm{)}}\mathrm{(}a\mathrm{=}a\mathrm{)}$, denoted $n\mathrm{\mapsto }{p}^n$, defined by

$p^0$$:\equiv {\mathrm{𝗋𝖾𝖿𝗅}}_{\mathrm{𝖻𝖺𝗌𝖾}}$

$p^{n+1}$$:\equiv p^{n}p$for $n\mathrm{\ge }\mathrm{0}$

$p^{n-1}$$:\equiv p^n{p}^{-1}$for $n\mathrm{\le }\mathrm{0}$.

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