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\mathsf{Prop}$ a family of mere propositions (a mere relation). Its quotient should be the set-coequalizer of the two projections

\mathchoice{{\textstyle\sum_{(a,b:A)}}}{\sum_{(a,b:A)}}{\sum_{(a,b:A)}}{\sum_{% (a,b:A)}}R(a,b)\rightrightarrows 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:A\to A/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\;\Bigl{(}\mathchoice{\sum_{(f:A\to B)}\,}{\mathchoice{{% \textstyle\sum_{(f:A\to B)}}}{\sum_{(f:A\to B)}}{\sum_{(f:A\to B)}}{\sum_{(f:A% \to B)}}}{\mathchoice{{\textstyle\sum_{(f:A\to B)}}}{\sum_{(f:A\to B)}}{\sum_{% (f:A\to B)}}{\sum_{(f:A\to B)}}}{\mathchoice{{\textstyle\sum_{(f:A\to B)}}}{% \sum_{(f:A\to B)}}{\sum_{(f:A\to B)}}{\sum_{(f:A\to B)}}}\mathchoice{\prod_{(a% ,b:A)}\,}{\mathchoice{{\textstyle\prod_{(a,b:A)}}}{\prod_{(a,b:A)}}{\prod_{(a,% b:A)}}{\prod_{(a,b:A)}}}{\mathchoice{{\textstyle\prod_{(a,b:A)}}}{\prod_{(a,b:% A)}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}}{\mathchoice{{\textstyle\prod_{(a,b:A)}% }}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}}R(a,b)\to(f(a)=f(b))% \Bigr{)}.

Proof.

The quasi-inverse of $\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}\circ q$ , going from right to left, is just the recursion principle for $A/R$ . That is, given $f:A\to B$ such that $\mathchoice{\prod_{a,b:A}\,}{\mathchoice{{\textstyle\prod_{(a,b:A)}}}{\prod_{(% a,b:A)}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}}{\mathchoice{{\textstyle\prod_{(a,b% :A)}}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}}{\mathchoice{{% \textstyle\prod_{(a,b:A)}}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}% }R(a,b)\to(f(a)=f(b)),$ we define $\bar{f}:A/R\to B$ by $\bar{f}(q(a)):\!\!\equiv f(a)$ . This defining equation says precisely that $(f\mapsto\bar{f})$ is a right inverse to $(\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}\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: $\mathchoice{\prod_{a:A}\,}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)% }}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod% _{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}% }{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}R(a,a)$ ,
•

symmetry: $\mathchoice{\prod_{a,b:A}\,}{\mathchoice{{\textstyle\prod_{(a,b:A)}}}{\prod_{(% a,b:A)}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}}{\mathchoice{{\textstyle\prod_{(a,b% :A)}}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}}{\mathchoice{{% \textstyle\prod_{(a,b:A)}}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}% }R(a,b)\to R(b,a)$ , and
•

transitivity: $\mathchoice{\prod_{a,b,c:C}\,}{\mathchoice{{\textstyle\prod_{(a,b,c:C)}}}{% \prod_{(a,b,c:C)}}{\prod_{(a,b,c:C)}}{\prod_{(a,b,c:C)}}}{\mathchoice{{% \textstyle\prod_{(a,b,c:C)}}}{\prod_{(a,b,c:C)}}{\prod_{(a,b,c:C)}}{\prod_{(a,% b,c:C)}}}{\mathchoice{{\textstyle\prod_{(a,b,c:C)}}}{\prod_{(a,b,c:C)}}{\prod_% {(a,b,c:C)}}{\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:A\to\mathsf{Prop}$ is an equivalence class of a relation $R:A\times A\to\mathsf{Prop}$ if there merely exists an $a : A$ such that for all $b : A$ we have $R(a,b)\simeq P(b)$ .

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\sslash R:\!\!\equiv\setof{P:A\to\mathsf{Prop}|P\text{ is an equivalence % class of }R}.

The function $q^{\prime}:A\to A\sslash R$ is defined by $q^{\prime}(a):\!\!\equiv P_{a}$ .

Theorem 6.10.6.

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

Proof.

First, note that if $R(a,b)$ , then since $R$ is an equivalence relation we have $R(a,c)\Leftrightarrow 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\sslash 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\sslash 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\sslash R$ raises universe level: if $A:\mathcal{U}_{i}$ and $R:A\to A\to\mathsf{Prop}_{\mathcal{U}_{i}}$ , then in the definition of $A\sslash R$ we must also use $\mathsf{Prop}_{\mathcal{U}_{i}}$ to include all the equivalence classes, so that $A\sslash R:\mathcal{U}_{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 $\mathbb{Z}$ as a set-quotient

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

where $\sim$ is the equivalence relation defined by

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

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\to A$ is called idempotent if $r\circ r=r$ .)

Lemma 6.10.8.

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

(A/{\sim}):\!\!\equiv\mathchoice{\sum_{x:A}\,}{\mathchoice{{\textstyle\sum_{(x% :A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_% {(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle% \sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}r(x)=x

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

\mathchoice{\sum_{(g:A\to B)}\,}{\mathchoice{{\textstyle\sum_{(g:A\to B)}}}{% \sum_{(g:A\to B)}}{\sum_{(g:A\to B)}}{\sum_{(g:A\to B)}}}{\mathchoice{{% \textstyle\sum_{(g:A\to B)}}}{\sum_{(g:A\to B)}}{\sum_{(g:A\to B)}}{\sum_{(g:A% \to B)}}}{\mathchoice{{\textstyle\sum_{(g:A\to B)}}}{\sum_{(g:A\to B)}}{\sum_{% (g:A\to B)}}{\sum_{(g:A\to B)}}}\mathchoice{\prod_{(x,y:A)}\,}{\mathchoice{{% \textstyle\prod_{(x,y:A)}}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}% }{\mathchoice{{\textstyle\prod_{(x,y:A)}}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}{% \prod_{(x,y:A)}}}{\mathchoice{{\textstyle\prod_{(x,y:A)}}}{\prod_{(x,y:A)}}{% \prod_{(x,y:A)}}{\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:\mathchoice{\prod_{x:A}\,}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:% A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{% \prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x% :A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\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,\mathord{\hskip 1.0pt\underline{\hskip 4.3pt}\hskip 1% .0pt}),

where the underscore $\mathord{\hskip 1.0pt\underline{\hskip 4.3pt}\hskip 1.0pt}$ 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 opposite direction,

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\mathsf{pr}_{1})\equiv(f\circ\mathsf{pr}_{1}% \circ q,{\mathord{\hskip 1.0pt\underline{\hskip 4.3pt}\hskip 1.0pt}}).

Because $B$ is a set we need not worry about the $\mathord{\hskip 1.0pt\underline{\hskip 4.3pt}\hskip 1.0pt}$ part, while for the first component we have

f(\mathsf{pr}_{1}(q(x))):\!\!\equiv f(r(x))=f(x),

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

Corollary 6.10.10.

Suppose $p:A\to B$ is a retraction between sets. Then $B$ is the quotient of $A$ by the equivalence relation $\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 $\mathbb{Z}$ with the idempotent $r:\mathbb{N}\times\mathbb{N}\to\mathbb{N}\times\mathbb{N}$ defined by

r(a,b)=\begin{cases}(a-b,0)&\text{if $a\geq b$,}\\ (0,b-a)&\text{otherwise.}\end{cases}

(This is a valid definition even constructively, since the relation $\geq$ on $\mathbb{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:\mathbb{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:\mathbb{Z}\to\mathcal{U}$ is a type family and that we have

•

$d_{0}:P(0)$ ,
•

$d_{+}:\mathchoice{\prod_{n:\mathbb{N}}\,}{\mathchoice{{\textstyle\prod_{(n:% \mathbb{N})}}}{\prod_{(n:\mathbb{N})}}{\prod_{(n:\mathbb{N})}}{\prod_{(n:% \mathbb{N})}}}{\mathchoice{{\textstyle\prod_{(n:\mathbb{N})}}}{\prod_{(n:% \mathbb{N})}}{\prod_{(n:\mathbb{N})}}{\prod_{(n:\mathbb{N})}}}{\mathchoice{{% \textstyle\prod_{(n:\mathbb{N})}}}{\prod_{(n:\mathbb{N})}}{\prod_{(n:\mathbb{N% })}}{\prod_{(n:\mathbb{N})}}}P(n)\to P(\mathsf{succ}(n))$ , and
•

$d_{-}:\mathchoice{\prod_{n:\mathbb{N}}\,}{\mathchoice{{\textstyle\prod_{(n:% \mathbb{N})}}}{\prod_{(n:\mathbb{N})}}{\prod_{(n:\mathbb{N})}}{\prod_{(n:% \mathbb{N})}}}{\mathchoice{{\textstyle\prod_{(n:\mathbb{N})}}}{\prod_{(n:% \mathbb{N})}}{\prod_{(n:\mathbb{N})}}{\prod_{(n:\mathbb{N})}}}{\mathchoice{{% \textstyle\prod_{(n:\mathbb{N})}}}{\prod_{(n:\mathbb{N})}}{\prod_{(n:\mathbb{N% })}}{\prod_{(n:\mathbb{N})}}}P(-n)\to P(-\mathsf{succ}(n))$ .

Then we have $f:\mathchoice{\prod_{z:\mathbb{Z}}\,}{\mathchoice{{\textstyle\prod_{(z:\mathbb% {Z})}}}{\prod_{(z:\mathbb{Z})}}{\prod_{(z:\mathbb{Z})}}{\prod_{(z:\mathbb{Z})}% }}{\mathchoice{{\textstyle\prod_{(z:\mathbb{Z})}}}{\prod_{(z:\mathbb{Z})}}{% \prod_{(z:\mathbb{Z})}}{\prod_{(z:\mathbb{Z})}}}{\mathchoice{{\textstyle\prod_% {(z:\mathbb{Z})}}}{\prod_{(z:\mathbb{Z})}}{\prod_{(z:\mathbb{Z})}}{\prod_{(z:% \mathbb{Z})}}}P(z)$ such that $f(0)\equiv d_{0}$ and $f(\mathsf{succ}(n))\equiv d_{+}(f(n))$ , and $f(-\mathsf{succ}(n))\equiv d_{-}(f(-n))$ for all $n:\mathbb{N}$ .

Proof.

We identify $\mathbb{Z}$ with $\mathchoice{\sum_{x:\mathbb{N}\times\mathbb{N}}\,}{\mathchoice{{\textstyle\sum% _{(x:\mathbb{N}\times\mathbb{N})}}}{\sum_{(x:\mathbb{N}\times\mathbb{N})}}{% \sum_{(x:\mathbb{N}\times\mathbb{N})}}{\sum_{(x:\mathbb{N}\times\mathbb{N})}}}% {\mathchoice{{\textstyle\sum_{(x:\mathbb{N}\times\mathbb{N})}}}{\sum_{(x:% \mathbb{N}\times\mathbb{N})}}{\sum_{(x:\mathbb{N}\times\mathbb{N})}}{\sum_{(x:% \mathbb{N}\times\mathbb{N})}}}{\mathchoice{{\textstyle\sum_{(x:\mathbb{N}% \times\mathbb{N})}}}{\sum_{(x:\mathbb{N}\times\mathbb{N})}}{\sum_{(x:\mathbb{N% }\times\mathbb{N})}}{\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\mathcal{U}$ . We can construct $g:\mathchoice{\prod_{x:\mathbb{N}\times\mathbb{N}}\,}{\mathchoice{{\textstyle% \prod_{(x:\mathbb{N}\times\mathbb{N})}}}{\prod_{(x:\mathbb{N}\times\mathbb{N})% }}{\prod_{(x:\mathbb{N}\times\mathbb{N})}}{\prod_{(x:\mathbb{N}\times\mathbb{N% })}}}{\mathchoice{{\textstyle\prod_{(x:\mathbb{N}\times\mathbb{N})}}}{\prod_{(% x:\mathbb{N}\times\mathbb{N})}}{\prod_{(x:\mathbb{N}\times\mathbb{N})}}{\prod_% {(x:\mathbb{N}\times\mathbb{N})}}}{\mathchoice{{\textstyle\prod_{(x:\mathbb{N}% \times\mathbb{N})}}}{\prod_{(x:\mathbb{N}\times\mathbb{N})}}{\prod_{(x:\mathbb% {N}\times\mathbb{N})}}{\prod_{(x:\mathbb{N}\times\mathbb{N})}}}Q(x)$ by double induction on $n$ :

	$\displaystyle g(0,0)$	$\displaystyle:\!\!\equiv d_{0},$
	$\displaystyle g(\mathsf{succ}(n),0)$	$\displaystyle:\!\!\equiv d_{+}(g(n,0)),$
	$\displaystyle g(0,\mathsf{succ}(m))$	$\displaystyle:\!\!\equiv d_{-}(g(0,m)),$
	$\displaystyle g(\mathsf{succ}(n),\mathsf{succ}(m))$	$\displaystyle:\!\!\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 : A$ and $p:a=a$ . There is a function $\mathchoice{\prod_{n:\mathbb{Z}}\,}{\mathchoice{{\textstyle\prod_{(n:\mathbb{Z% })}}}{\prod_{(n:\mathbb{Z})}}{\prod_{(n:\mathbb{Z})}}{\prod_{(n:\mathbb{Z})}}}% {\mathchoice{{\textstyle\prod_{(n:\mathbb{Z})}}}{\prod_{(n:\mathbb{Z})}}{\prod% _{(n:\mathbb{Z})}}{\prod_{(n:\mathbb{Z})}}}{\mathchoice{{\textstyle\prod_{(n:% \mathbb{Z})}}}{\prod_{(n:\mathbb{Z})}}{\prod_{(n:\mathbb{Z})}}{\prod_{(n:% \mathbb{Z})}}}(a=a)$ , denoted $n\mapsto p^{n}$ , defined by

$\displaystyle p^{0}$	$\displaystyle:\!\!\equiv\mathsf{refl}_{\mathsf{base}}$
$\displaystyle p^{n+1}$	$\displaystyle:\!\!\equiv p^{n}\mathchoice{\mathbin{\raisebox{2.15pt}{$% \displaystyle\centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{% \mathbin{\raisebox{1.075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox% {0.43pt}{$\scriptscriptstyle\,\centerdot\,$}}}p$	for $n\geq 0$
$\displaystyle p^{n-1}$	$\displaystyle:\!\!\equiv p^{n}\mathchoice{\mathbin{\raisebox{2.15pt}{$% \displaystyle\centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{% \mathbin{\raisebox{1.075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox% {0.43pt}{$\scriptscriptstyle\,\centerdot\,$}}}\mathord{{p}^{-1}}$	for $n\leq 0$ .

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

Title	6.10 Quotients
\metatable