From f8a57c3d580747bd6099fd877a9d779f4b0c06ce Mon Sep 17 00:00:00 2001 From: Alex Gryzlov Date: Tue, 8 Aug 2023 05:31:54 +0200 Subject: [PATCH] fix xca:ints-as-quotient --- intro-uf.tex | 24 ++++++++++++------------ 1 file changed, 12 insertions(+), 12 deletions(-) diff --git a/intro-uf.tex b/intro-uf.tex index 2193e1e..69604ae 100644 --- a/intro-uf.tex +++ b/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,7 +1884,7 @@ \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$ @@ -1892,7 +1892,7 @@ \section{Univalence}\label{sec:univax} 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{%