fix xca:ints-as-quotient

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{%