errata.tex

% This is the errata document for the homotopy type theory book.

% This file supports two book sizes:
% - Letter size (8.5" x 11")
% - US Trade size (6" x 9")
%
% To activate one or the other, uncomment the appropriate font size in
% the documentclass below, and then one of the two page geometry incantations
%
% NOTE: The 6" x 9" format is only experimental. It will break the
% title page, for example.

\PassOptionsToPackage{table}{xcolor}

% DOCUMENT CLASS
\documentclass[
%
%10pt % for US Trade 6" x 9" book
%
11pt % for Letter size book
]{article}
\usepackage{etex} % We're running out of registers and dimensions, or some such

\newcounter{chapter}            % So that macros.tex doesn't choke

% PAGE GEOMETRY
%
% Uncomment one of these

% We make the page 40pt taller than the standard LaTeX book.

% OPTION 1: Letter
\usepackage[papersize={8.5in,11in},
            twoside,
            includehead,
            top=1in,
            bottom=1in,
            inner=0.75in,
            outer=1.0in,
            bindingoffset=0.35in]{geometry}

% OPTION 2: US Trade
% \usepackage[papersize={6in,9in},
%             twoside,
%             includehead,
%             top=0.75in,
%             bottom=0.75in,
%             inner=0.5in,
%             outer=0.75in,
%             bindingoffset=0.35in]{geometry}

% HYPERLINKING AND PDF METADATA

\usepackage[pagebackref,
            colorlinks,
            citecolor=darkgreen,
            linkcolor=darkgreen,
            unicode,
            pdfauthor={Univalent Foundations Program},
            pdftitle={Homotopy Type Theory: Univalent Foundations of Mathematics},
            pdfsubject={Mathematics},
            pdfkeywords={type theory, homotopy theory, univalence axiom}]{hyperref}

% OTHER PACKAGES

% Use this package and stick \layout somewhere in the text to see
% page margins, text size and width etc. Useful for debugging page format.
%\usepackage{layout}

%%% Because Germans have umlauts and Slavs have even stranger ways of mangling letters
\usepackage[utf8]{inputenc}

%%% For table {tab:theorems}
\usepackage{pifont}

%%% Multi-Columns for long lists of names
\usepackage{multicol}

%%% Set the fonts
\usepackage{mathpazo}
\usepackage[scaled=0.95]{helvet}
\usepackage{courier}
\linespread{1.05} % Palatino looks better with this

\usepackage{graphicx}
\usepackage{comment}

\usepackage{wallpaper} % For the background image on the cover page

\usepackage{fancyhdr} % To set headers and footers

\usepackage{nextpage} % So we can jump to odd-numbered pages

\usepackage{amssymb,amsmath,amsthm,stmaryrd,mathrsfs,wasysym}
\usepackage{enumitem,mathtools,xspace}
\usepackage{xcolor} % For colored cells in tables we need \cellcolor
\usepackage{booktabs} % For nice tables
\usepackage{array} % For nice tables
\usepackage{supertabular} % For index of symbols
\definecolor{darkgreen}{rgb}{0,0.45,0}
\usepackage{aliascnt}
\usepackage[capitalize]{cleveref}
\usepackage[all,2cell]{xy}
\UseAllTwocells
\usepackage{natbib}
\usepackage{braket} % used for \setof{ ... } macro
\usepackage{tikz}
\usetikzlibrary{decorations.pathmorphing}

\usepackage{etoolbox}           % hacking commands for TOC

\usepackage{mathpartir}         % for formal.tex appendix, section 3

\usepackage[numbered]{bookmark} % add chapter/section numbers to the toc in the pdf metadata

\input{macros}

%%%% Indexing
\usepackage{makeidx}
\makeindex

%%%% Header and footers
\pagestyle{fancyplain}
\setlength{\headheight}{15pt}
\renewcommand{\sectionmark}[1]{\markright{\textsc{\thesection\ #1}}}

\lhead[\fancyplain{}{{\thepage}}]%
      {\fancyplain{}{\nouppercase{\rightmark}}}
\rhead[\fancyplain{}{\nouppercase{\leftmark}}]%
      {\fancyplain{}{\thepage}}
\cfoot[]{}
\lfoot[]{}
\rfoot[]{}

%%%% Chapter & part style
\usepackage{titlesec}
\titleformat{\part}[display]{\fontsize{40}{40}\fontseries{m}\fontshape{sc}\selectfont}{\hfil\partname\ \Roman{part}}{20pt}{\fontsize{60}{60}\fontseries{b}\fontshape{sc}\selectfont\hfil}
\titleformat{\chapter}[display]{\fontsize{23}{25}\fontseries{m}\fontshape{it}\selectfont}{\chaptertitlename\ \thechapter}{20pt}{\fontsize{35}{35}\fontseries{b}\fontshape{n}\selectfont}

\input{main.labels}
\input{version.tex}

\usepackage{longtable}

\title{Errata for the HoTT Book, first edition%
%% VERSION MARKER
}

\begin{document}
\maketitle

For the benefit of all readers, the available PDF and printed copies of the book are being updated on a rolling basis with minor corrections and clarifications as we receive them. Every copy has a version marker that can be found on the title page and is of the form "first-edition-XX-gYYYYYYY", where XX is a natural number and YYYYYYY is the git commit hash that uniquely identifies the exact version. Higher values of XX indicate more recent copies.

Below is a list of corrections and clarifications that have been made
%% BEGIN STARTPOINT
so far
%% END STARTPOINT
(except for trivial formatting and spacing changes), along with the version marker in which they were first made.
This list is current as of \today\ and version marker ``\OPTversion''.

While the page numbering may differ between copies with different version markers (and indeed, already differs between the letter/A4 and printed/ebook copies with the same version marker), we promise that the numbering of chapters, sections, theorems, and equations will remain constant, and no new mathematical content will be added, unless and until there is a second edition.

\noindent
\begin{longtable}{llp{10.5cm}}
  \textbf{Location} & \textbf{Fixed in} & \textbf{Change} \\ \hline \endhead
%% BEGIN ERRATA
  %
  % Chapter 1
  %
  \autoref{sec:types-vs-sets}
  & 182-gb29ea2f
  & Change notation $a\jdeq_A b$ to $a\jdeq b : A$, to match that used in \autoref{cha:rules}.
  (Neither are used anywhere else in the book.)\\
  %
  \autoref{sec:types-vs-sets}
  & 154-g42698c2
  & Clarify that algorithmic decidability of judgmental equality is only meta-theoretic.\\
  %
  \autoref{sec:types-vs-sets}
  & 154-gac9b226
  & Mention notation $a=b=c=d$ to mean ``$a=b$ and $b=c$ and $c=d$, hence $a=d$'', possibly including judgmental equalities.\\
  %
  \autoref{sec:universes}
  & 42-g4bc5cc2
  & Cumulativity means some elements do not have unique types, the index $i$ on $\UU_i$ is not an internal natural number, and typical ambiguity must be justified by reinserting indices.\\
  %
  \autoref{sec:universes,sec:pi-types}
  & 42-ga34b313
  & Explain that we can't define $\Fin$ and $\fmax$ yet where we first mention them.\\
  %
  \autoref{sec:pi-types}
  & 165-g0ad2aba
  & Add $\mathsf{swap}$ as another example of a polymorphic function, and discuss the use of subscripts and implicit arguments to dependent functions.\\
  %
  \autoref{rmk:introducing-new-concepts}
  & 80-g8f95fa5
  & In the discussion of formation rules, the dependent function type example should be $\prd{x:A} B(x)$.\\
  %
  \autoref{sec:finite-product-types}
  & 51-g67e86db
  & Better explanation of recursion on product types, why it is justified, and how it relates to the uniqueness principle.\\
  %
  \autoref{sec:sigma-types}
  & 2-gbe277a8
  & In the types of $g$ and $\ind{\sm{x:A}B(x)}$, there is a $\prd{a:A}{b:B(x)}$ in which $x$ should be $a$.\\
  %
  \autoref{sec:sigma-types}
  & 27-gd0bfa0d
  & At two places in the definition of $\ac$, $R(a,\fst(g(x)))$ should be $R(x,\fst(g(x)))$.\\
  %
  \autoref{sec:sigma-types}
  & 125-g7fdadbf
  & When substituting $\lam{x} \fst(g(x))$ for $f$ while verifying that $\ac$ is well-typed, the left side of the judgmental equality should be $\tprd{x:A} R(x,\fst(g(x)))$, not $\tprd{x:A} R(x,\fst(f(x)))$.\\
  %
  \autoref{sec:coproduct-types}
  & 30-g264d934
  & In two displayed equations, $f(\inl(b))$ should be $f(\inr(b))$.\\
  %
  \autoref{sec:type-booleans}
  & 125-g433f87e
  & In the definition of binary products in terms of $\bool$, the definitions of $\fst(p)$ and $\snd(p)$ should be switched to match the order of arguments to $\rec\bool$ and $\ind\bool$.\\
  % 
  \autoref{sec:pat}
  & 111-g1e868fa
  & When translating English to type theory, ``unnamed variables'' are unnamed in English but must be named in type theory.\\
  %
  \autoref{sec:identity-types}
  & 154-g4ef49f7
  & Emphasize that path induction, like all other induction principles, defines a \emph{specified} function.\\
  %
  \autoref{sec:identity-types}
  & 244-gd58529d
  & In proof that path induction implies based path induction, $D(x,y,p)$ should be written $\prd{C : \prd{z:A} (\id[A]{x}{z}) \to \UU} \left( \cdots \right)$ so the type of $C$ matches the premise of based path induction. \\
  %
  \autoref{ex:iterator}
  & 78-gcce4dc0
  & The second defining equation of $\ite$ should have right-hand side $c_s(\ite(C,c_0,c_s,n))$.\\
  %
  \autoref{ex:prod-via-bool}
  & 229-ged891f3
  & This exercise requires function extensionality (\autoref{sec:compute-pi}).\\
  %
  \autoref{ex:ackermann}
  & 110-gfe4641b
  & To match the usual Ackermann--P\'eter function, the second displayed equation should be $\ack(\suc(m),0) \jdeq \ack(m,1)$.\\
  %
  % Chapter 2
  %
  \autoref{cha:basics}
  & 239-gaf3d682
  & In the chapter introduction, clarify that topological homotopies between paths must be endpoint-preserving.\\
  %
  \autoref{lem:opp}
  & 166-g37b78ef
  & Add remarks before and after the proof about how a theorem's statement and proof should be interpreted as exhibiting an element of some type.\\
  %
  \autoref{sec:equality}
  & 165-g18642ca
  & Mention that the notation $a=b=c=d$, and its displayed variant, indicate concatenation of paths.\\
  %
  \autoref{sec:equality}
  & 253-gdd47c75
  & \autoref{thm:omg}\ref{item:omg4} justifies writing $p\ct q \ct r$ and so on.\\
  %
  \autoref{thm:EckmannHilton}
  & 253-gdd47c75
  & The induction defining $\alpha\rightwhisker r$ has defining equation $\alpha \rightwhisker \refl{b} \jdeq \opp{\mathsf{ru}_p} \ct \alpha \ct \mathsf{ru}_q$, with $\mathsf{ru}_p$ the right unit law.
  For $\alpha\hct\beta = \alpha\ct\beta$ to be well-typed, we assume $p\jdeq q \jdeq r \jdeq s\jdeq \refl{a}$ and use $\mathsf{ru}_{\refl{a}} = \refl{\refl{a}}$ and its dual.
  Proving $\alpha\hct\beta = \alpha\hct'\beta$ requires induction not only on $\alpha$ and $\beta$ but then on the two remaining 1-paths.
  After the proof, remark that we trust the reader to construct such operations from now on.\\
  %
  \autoref{def:loopspace}
  & 233-gc3fb777
  & The three displays should be $\defeq$'s rather than $=$'s.\\
  %
  \autoref{sec:fibrations}
  & 154-g4ef49f7
  & Emphasize that unlike fibrations in classical homotopy theory, type families come with a \emph{specified} path-lifting function.\\
  %
  \autoref{cor:hom-fg}
  & 253-gdd47c75
  & Canceling $H(x)$ may be done by whiskering with $\opp{(H(x))}$.\\
  %
  \autoref{sec:compute-cartprod}
  & 74-g9896e32
  & In the type of $\pairpath$ (just after the proof of \autoref{thm:path-prod}), the second factor in the domain should be $\id{\proj{2}(x)}{\proj{2}(y)}$.\\
  %
  \autoref{thm:trans-prod}
  & 76-ga42354c
  & The third displayed judgmental equality in the proof should be $\transfib{B}{p}{\proj{2}x} \jdeq \proj2x$.\\
  %
  \autoref{sec:compute-paths}
  & 236-g32be999
  & The second display after the proof of \autoref{thm:paths-respects-equiv} should be $\prd{x:A} (\id[f(x)=g(x)] {\happly(p)(x)}{\happly(q)(x)})$.\\
  %
  \autoref{sec:compute-coprod}
  & 101-g645f763
  & In \autoref{thm:path-coprod} and the preceding paragraph, in the equivalence $\eqv{(\inl(a)=x)}{\code(x)}$, the variable $a$ should be $a_0$. \\
  %
  % Chapter 3
  %
  \autoref{subsec:prop-subsets}
  & 86-g39feab1
  & The definition of subset containment should say $\prd{x:A}(P(x)\rightarrow Q(x))$, not $\fall{x:A}(P(x)\Rightarrow Q(x))$, as the latter notation has not been introduced yet.\\
  %
  \autoref{thm:retract-contr}
  & 95-gce0131f
  & In the proof, $p$ should be $r$ to match the preceding definition of retraction.\\
  %
  % Chapter 4
  %
  \autoref{lem:qinv-autohtpy}
  & 87-g693e9b9
  & At the end of the proof, \autoref{thm:contr-paths} should be cited as the reason why $\sm{g:A\to A} (g = \idfunc[A])$ is contractible.\\
  %
  \autoref{fibwise-fiber-total-fiber-equiv}
  & 202-g775a3f0
  & The last equivalence in the proof is not by~\eqref{eq:path-lump} but by \autoref{thm:omit-contr,thm:contr-paths,ex:sigma-assoc}.\\
  %
  \autoref{thm:nobject-classifier-appetizer}
  & 205-gf9fe386
  & In the proof, $e\cdot \proj1$ should be $\trans{(\ua(e))}{\proj1}$.  Also, explain its computation better.\\
  %
  \autoref{sec:univalence-implies-funext}
  & 114-gaba76c8
  & The point of \autoref{UA-eqv-hom-eqv} is that it follows from univalence without assuming function extensionality separately.\\
  %
  % Chapter 5
  %
  \autoref{sec:w-types}
  & 125-g433f87e
  & Use $\bfalse$ for $0$ and $\btrue$ for $\suc$, to match the ordering of $\bfalse$ and $\btrue$ in \autoref{sec:type-booleans}.\\
  %
  \autoref{sec:w-types}
  & 218-g42219cb
  & In the description of the constructor $\supp$, its second argument is more clearly written as $f : B(a) \to \wtype{x:A} B(x)$.\\
  %
  \autoref{thm:identity-systems}
  & 139-gd5c5d01
  & In the proof of \ref{item:identity-systems4}$\Rightarrow$\ref{item:identity-systems1}, the type of $D'$ should be $(\sm{b:A} R(b)) \to \type$.\\
  %
  % Chapter 6
  %
  \autoref{sec:dependent-paths}
  & 54-gd4a47c2
  & Soon after \autoref{rmk:defid}, the phrase ``An element $b:P(\base)$ in the fiber over the constructor $\base:\nat$'' should say $\base:\Sn^1$.\\
  %
  % Chapter 7
  %
  \autoref{thm:h-level-retracts}
  & 180-gb672a4d
  & In the last displayed equation of the proof, $q$ should be $r$.\\
  %
  \autoref{thm:isaprop-isofhlevel}
  & 101-g713f48c
  & The base case in the proof is just \autoref{thm:isprop-iscontr}.\\
  %
  \autoref{ex:s2-colim-unit}
  & 101-ga366be2
  & ``entires'' should be ``entirely''.\\
  %
  % Chapter 8
  %
  \autoref{thm:hopf-fibration}
  & 256-g9e6fcb8
  & The phrase ``whose fibers are $\Sn^1$'' should be ``whose fiber over the basepoint is $\Sn ^1$''.
  The same change should be made in \autoref{ex:HopfJr,ex:SuperHopf}.\\
  %
  \autoref{thm:freudcode}
  & 87-g3f977b2
  & In the second displayed equation in the proof, $\merid(x_1)$ should be $\opp{\merid(x_1)}$.\\
  %
  \autoref{thm:freudlemma}
  & 88-g0c0be67
  & The type of $m$ should be $a_1=a_2$, the second display should begin with $C(a_1,\transfib{B}{\opp m}{b})$, and the proof should say ``we may assume $a_2$ is $a_1$ and $m$ is $\refl{a_1}$''.\\
  %
  \autoref{sec:freudenthal}
  & 165-gd5584c6
  & In~\eqref{eq:freudcompute1}, $r''$ should be $r'$, the end point of $r$ should be $\transfib{B}{\opp{\merid(x_0)}}{q}$, and obtaining $r'$ requires also identifying this with $q \ct \opp{\merid(x_0)}$.
  Similarly, in~\eqref{eq:freudcompute2}, the end point of $r$ should be $\transfib{B}{\opp{\merid(x_1)}}{q}$.\\
  %
  % Chapter 9
  %
  %
  % Chapter 10
  %
  \autoref{thm:ordord}
  & 140-g55de417
  & The second sentence of the proof should say ``By well-founded induction on $A$, suppose $\ordsl A b$ is accessible for all $b<a$.''\\
  %
  \autoref{thm:ordunion}
  & 140-gd7f8960
  & The statement should say $X:\UU$ rather than $X:\UU_\UU$.\\
  %
  \autoref{thm:wellorder}
  & 140-gcca0bcf
  & The penultimate sentence of the proof should say ``if $a<b$ and $b<c$'' rather than ``if $a<b$ and $a<c$''.\\
  %
  % Chapter 11
  %
  \autoref{dedekind-in-cut-as-le}
  & 165-gb002a64
  & The statement should say ``For all $x : \RD$ and $q : \Q$, $L_x(q) \Leftrightarrow (q < x)$ and $U_x(q)
  \Leftrightarrow (x < q)$.''\\
  %
  \autoref{RD-inverse-apart-0}
  & 165-g179b359
  & In the proof, the sentence beginning ``From $0<ac$ it follows'' should be replaced by ``From $0 < a c$ and $0 < b c$ it follows
  that $a$, $b$, and $c$ are either all positive or all negative.
  Hence either $0 < a < x$ or $x < b < 0$, so that $x \apart 0$.''\\
  %
  \autoref{lem:untruncated-linearity-reals-coincide}
  & 87-g82b27c3
  & \eqref{eq:untruncated-linearity} should be $c:\prd{q, r : \Q} (q < r) \to (q < x) + (x < r)$, and therefore the use of $c$ in the proof should be $c(s,t)$ rather than $c(x,s,t)$.\\
  %
  \autoref{ex:mean-value-theorem}
  & 222-g3453cf1
  & This is the intermediate value theorem, not the mean value theorem.\\
  %
  % Appendix A
  %
  \autoref{cha:rules}
  & 165-g76db618
  & After the introduction of the judgment ``$\wfctx{\Gamma}$'' in the Preliminaries, the sentence beginning ``Therefore, if $\oftp\Gamma aA$, \dots'' should say instead ``In particular, therefore, if $\oftp\Gamma aA$, \dots''.\\
  %
  \autoref{subsec:contexts}
  & 64-g7c2312e
  & Clarify the distinction between typing judgments and context well-formedness judgments, and
  remove the $\vdash$ from the notation for the latter.\\
  %
  \autoref{sec:more-formal-sigma}
  & 26-gcd691e8
  & In $\Sigma$-\comp\ and the following paragraph, $y.C$ should be $z.C$, and ``we bind \dots $y$ in $C$'' should likewise say $z$.\\
%% END ERRATA
\end{longtable}

\end{document}