fix xca:ints-as-quotient and lem:euclid-div, clarify lem:PHP

intro-uf.tex

@@ -1407,8 +1407,8 @@ \section{Equivalences}\label{sec:equivalence}
 
 \begin{xca}\label{xca:prod-of-fibs}
   Let $X$, $Y$ and $Z$ be types. Given functions $f: X\to Z$ and $g: Y\to Z$,
-  construct an equivalence of type 
-  $(\sum_{h:X\to Y} f \eqto g\circ h) \equivto 
+  construct an equivalence of type
+  $(\sum_{h:X\to Y} f \eqto g\circ h) \equivto
     \prod_{x:X}\sum_{y:Y} f(x) \eqto g(y)$.
   Hint: use \cref{def:funext}.
 \end{xca}
@@ -1884,15 +1884,15 @@ \subsection{Unary sums}\label{sec:unary-sum-types}
 
 \section{Univalence}\label{sec:univax}
 
-The univalence axiom, to be presented in this section, greatly enhances 
+The univalence axiom, to be presented in this section, greatly enhances
 our ability to produce identifications between the two types and to use the
 resulting identifications to transport (in the sense of \cref{def:transport})
 properties and structure between the types.  It asserts that if $\UU$
 is a universe, and $X$ and $Y$ are types in $\UU$, then a specific function,
 mapping identifications between $X$ and $Y$ to equivalences between
 $X$ and $Y$, is an equivalence.
 
-We now define the function that the univalence axiom postulates 
+We now define the function that the univalence axiom postulates
 to be an equivalence.
 
 \begin{definition}\label{def:idtoeq}
@@ -1917,7 +1917,7 @@ \section{Univalence}\label{sec:univax}
 \begin{principle}[Univalence Axiom]\label{def:univalence}
     Let $\UU$ be a universe.
     Voevodsky's \emph{univalence axiom}\index{univalence axiom} for $\UU$
-    postulates that $p\mapsto \ptoe p$ is an equivalence 
+    postulates that $p\mapsto \ptoe p$ is an equivalence
     of type $(X \eqto Y) \to (X\equivto Y)$, for all $X,Y:\UU$.
     Formally, we postulate the existence of a family of elements
     \[
@@ -1928,13 +1928,13 @@ \section{Univalence}\label{sec:univax}
     parameterized by $X,Y:\UU$.
 \end{principle}
 
-For an equivalence $f: X\equivto Y$, we will adopt the 
+For an equivalence $f: X\equivto Y$, we will adopt the
 notation $\etop f : X \eqto Y $ to denote $\inv{(p\mapsto\ptoe p)}(f)$,%
 \glossary(1bar){$\protect\etop f$}{path obtained by univalence from $f$}
-the result of applying the inverse function of $(p\mapsto\ptoe p)$, 
-given by $\ua_{X,Y}$, to $f$.  
-Thus there are identifications of type $\etop {\ptoe p} \eqto p$ 
-and $\ptoe {\etop f} \eqto f$.  There are also identifications of 
+the result of applying the inverse function of $(p\mapsto\ptoe p)$,
+given by $\ua_{X,Y}$, to $f$.
+Thus there are identifications of type $\etop {\ptoe p} \eqto p$
+and $\ptoe {\etop f} \eqto f$.  There are also identifications of
 type $\overetop{\id_X} \eqto \refl{X}$
 and $\overetop{g\,f} \eqto \etop{g}\,\etop{f}$ if $g: Y\equivto Z$.
 
@@ -1983,7 +1983,7 @@ \section{Heavy transport}
 as parameter type and type families $Y\defeq Z\defeq \id_\UU$.
 Then $Y\to Z$ is $X \mapsto (X\to X)$. Now,
 if $A,B:\UU$ and $e: A \eqto B$ comes from an equivalence $g:A\equivto B$
-by applying the univalence axiom, 
+by applying the univalence axiom,
 then the above construction combined with function extensionality
 yields that for any $f: A\to A$ (see the diagram in the margin)
 \[
@@ -3690,7 +3690,7 @@ \subsection{Set quotients}
 $R((w_1,d_1),(w_2,d_2)) \defeq  (w_1+d_2 = w_2 + d_1)$.
 Let $Z \defeq \set{(w,d)\mid (d=0) \lor (w=0 \land d\ne 0)}$.
 Construct an equivalence $f: A/R\to Z$ such that for all
-$(w,d,p):Z$ we have $f([(w,d)]) = (w,d)$.
+$((w,d),p):Z$ we have $f([(w,d)]) = ((w,d),p)$.
 \end{xca}
 
 It is also possible to postulate\footnote{%
@@ -3890,8 +3890,8 @@ \section{More on natural numbers}
 \end{remark}
 
 \begin{lemma}\label{lem:PHP}
-For all $N:\NN$ and $f:\NN\to\NN$ such that $f(n)<N$
-for all $n<N+1$, there exist $m < n < N+1$ such that $f(n) = f(m)$.
+For all $N:\NN$ and $f:\NN\to\NN$ such that $f(x)<N$
+for all $x<N+1$, there exist $m < n < N+1$ such that $f(n) = f(m)$.
 \end{lemma}
 \begin{proof}
 By induction on $N$. In the base case $N = 0$ there is nothing to do.
@@ -3900,7 +3900,7 @@ \section{More on natural numbers}
 that $f(n)<N+1$ for all $n<N+2$. The idea of the proof is
 to search for an $n<N+1$ such that $P(n)\defeq (f(n) = N)$,
 by computing $\mu_P(N+1)$ as in \cref{def:Nwellordered}.
-If $\mu_P(N+1) = N+1$, that is, $f(n)<N$ for all $n<N+1$,
+If $\mu_P(N+1) = N+1$, that is, $f(x)<N$ for all $x<N+1$,
 then we are done by IH. Assume $\mu_P(N+1) < N+1$,
 so $f(\mu_P(N+1)) = N$.
 If also $f(N+1) = N$ then we are done.
@@ -3928,7 +3928,7 @@ \section{More on natural numbers}
 \end{lemma}
 \begin{proof}
 Define $P(k)\defeq (n\leq km)$. Since $m>0$ we have $P(n)$.
-Now set $k\defeq\mu_P(n)$ as in \cref{def:Nwellordered}.
+Now set $k\defeq\mu_P(n+1)$ as in \cref{def:Nwellordered}.
 If $n = km$ and we set $q\defeq k$ and $r\defeq 0$.
 If $n<km$, then $k>0$ and we set $q\defeq k-1$.
 By minimality we have $qm<n<km$ and hence $n = qm+r$ for some $r<m$.