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}
\DeclareGraphicsExtensions{.png}
\input{bmpsize-hack} % for bounding boxes in dvi mode
\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{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
  %
  \cref{sec:types-vs-sets}
  & 182-gb29ea2f
  & Change notation $a\jdeq_A b$ to $a\jdeq b : A$, to match that used in \cref{cha:rules}.
  (Neither are used anywhere else in the book.)\\
  %
  \cref{sec:types-vs-sets}
  & 154-g42698c2
  & Clarify that algorithmic decidability of judgmental equality is only meta-theoretic.\\
  %
  \cref{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.\\
  %
  \cref{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.\\
  %
  \cref{sec:universes,sec:pi-types}
  & 42-ga34b313
  & Explain that we can't define $\Fin$ and $\fmax$ yet where we first mention them.\\
  %
  \cref{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.\\
  %
  \cref{rmk:introducing-new-concepts}
  & 80-g8f95fa5
  & In the discussion of formation rules, the dependent function type example should be $\prd{x:A} B(x)$.\\
  %
  \cref{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.\\
  %
  \cref{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$.\\
  %
  \cref{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)))$.\\
  %
  \cref{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)))$.\\
  %
  \cref{sec:coproduct-types}
  & 30-g264d934
  & In two displayed equations, $f(\inl(b))$ should be $f(\inr(b))$.\\
  %
  Theorem \ref{thm:allbool-trueorfalse} % NB: We have to write out "Theorem" instead of using \cref here, since in the (post-erratum) version this label no longer denotes a Theorem.
  & 391-g1ce619a
  & This should not be called a ``Theorem'', since we have not yet introduced what that means.
  Instead it should say ``We construct an element of\dots''.\\
  %
  \cref{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$.\\
  \cref{sec:pat}
  & 111-g1e868fa
  & When translating English to type theory, ``unnamed variables'' are unnamed in English but must be named in type theory.\\
  %
  \cref{sec:identity-types}
  & 154-g4ef49f7
  & Emphasize that path induction, like all other induction principles, defines a \emph{specified} function.\\
  %
  \cref{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. \\
  %
  \cref{rmk:the-only-path-is-refl}
  & 563-g3286941
  & The facts that any $(x,y,p): \sm{x,y:A}(\id{x}{y})$ is equal to $(x,x,\refl{x})$, and that any $(y,p):\sm{y:A}(\id[A]{a}{y})$ is equal to $(a,\refl{a})$, can be proven by path induction and based path induction respectively.\\
  %
  \cref{ex:iterator}
  & 78-gcce4dc0
  & The second defining equation of $\ite$ should have right-hand side $c_s(\ite(C,c_0,c_s,n))$.\\
  %
  \cref{ex:iterator}
  & 293-g4663bfe
  & The defining equations of the recursor derived from the iterator only hold propositionally, and require the induction principle to prove.\\
  %
  \cref{ex:prod-via-bool}
  & 229-ged891f3
  & This exercise requires function extensionality (\cref{sec:compute-pi}).\\
  %
  \cref{ex:nat-semiring}
  & 450-g7f38c9a
  & This exercise requires symmetry and transitivity of equality, \cref{lem:opp,lem:concat}.\\
  %
  \cref{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
  %
  \cref{cha:basics}
  & 239-gaf3d682
  & In the chapter introduction, clarify that topological homotopies between paths must be endpoint-preserving.\\
  %
  \cref{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.\\
  %
  \cref{lem:concat}
  & 374-g0bc0908
  & In the penultimate display in the first proof, $d(x,z,q)$ should be simply $d$.\\
  %
  \cref{thm:omg}
  & 750-g91b7348
  & In the first proofs of~\ref{item:omg1}--\ref{item:omg3}, $\indid{A}(D,d,p)$ should be $\indid{A}(D,d,x,y,p)$.\\
  %
  \cref{sec:equality}
  & 435-gee0b28a
  & In the third paragraph after \cref{lem:concat}, $p\ct\refl{x}\jdeq p$ should be $p\ct\refl{y}\jdeq p$.\\
  %
  \cref{sec:equality}
  & 165-g18642ca
  & Mention that the notation $a=b=c=d$, and its displayed variant, indicate concatenation of paths.\\
  %
  \cref{sec:equality}
  & 253-gdd47c75
  & \cref{thm:omg}\ref{item:omg4} justifies writing $p\ct q \ct r$ and so on.\\
  %
  \cref{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.\\
  %
  \cref{def:loopspace}
  & 233-gc3fb777
  & The three displays should be $\defeq$'s rather than $=$'s.\\
  %
  \cref{sec:functors}
  & 336-g8ff8a7f
  & In the type of $\apfunc{f}$ towards the end of the first proof of \cref{lem:map}, $g(x)$ should be $f(y)$.\\
  %
  \cref{sec:fibrations}
  & 154-g4ef49f7
  & Emphasize that unlike fibrations in classical homotopy theory, type families come with a \emph{specified} path-lifting function.\\
  %
  \cref{sec:fibrations}
  & 343-g6efd724
  & The functions \cref{eq:ap-to-apd} and \cref{eq:apd-to-ap} are obtained by concatenating with $\transconst Bp{f(x)}$ and its inverse, respectively.\\
  %
  \cref{cor:hom-fg}
  & 253-gdd47c75
  & Canceling $H(x)$ may be done by whiskering with $\opp{(H(x))}$.\\
  %
  \cref{sec:compute-cartprod}
  & 74-g9896e32
  & In the type of $\pairpath$ (just after the proof of \cref{thm:path-prod}), the second factor in the domain should be $\id{\proj{2}(x)}{\proj{2}(y)}$.\\
  %
  \cref{sec:compute-cartprod}
  & 895-g96db894
  & In the displayed equation just before \cref{thm:trans-prod}, $\pairct(p\ct q, r, p'\ct q', r)$ should be $\pairct(p\ct q, r, p'\ct q', r')$ and $\pairct(p, q\ct r, p', q'\ct r)$ should be $\pairct(p, q\ct r, p', q'\ct r')$ (two primes on $r$s are missing).\\
  %
  \cref{thm:trans-prod}
  & 349-gc7fd9d8
  & The path is in $A(w)\times B(w)$, not $A(y)\times B(y)$.\\
  %
  \cref{thm:trans-prod}
  & 76-ga42354c
  & The third displayed judgmental equality in the proof should be $\transfib{B}{p}{\proj{2}x} \jdeq \proj2x$.\\
  %
  \cref{thm:path-sigma}
  & 507-g8f10eda
  & In the proof, the equation $f(g(\refl{},\refl{}))=\refl{}$ should be $f (g(\refl{w_1},\refl{w_2})) = (\refl{w_1},\refl{w_2})$.\\
  %
  \cref{sec:compute-pi}
  & 269-g3880fe2
  & The paragraph preceding the definition of $\transfib{\Pi_A(B)}{p}{f}$ (before \cref{eq:transport-arrow-families}) misstated the (already given) type of $p$.\\
  %
  \cref{axiom:univalence}
  & 992-gc4a5314
  & The axiom should read ``For any $A,B:\type$, the function~\eqref{eq:uidtoeqv} is an equivalence.  The display $\eqv{(\id[\type]{A}{B})}{(\eqv A B)}$ should be deduced afterwards, outside the axiom statement.\\
  %
  \cref{thm:paths-respects-equiv}
  & 310-gd5fa240
  & The second half of the proof is more involved than the first.
  It follows abstractly using the 2-out-of-6 property (\cref{ex:2-out-of-6}), or more concretely by concatenating with $\opp{\alpha_{f(a)}} \ct {\alpha_{f(a)}}$ on each side and then repeatedly using naturality and functoriality.\\
  %
  \cref{sec:compute-paths}
  & 236-g32be999
  & The second display after the proof of \cref{thm:paths-respects-equiv} should be $\prd{x:A} (\id[f(x)=g(x)] {\happly(p)(x)}{\happly(q)(x)})$.\\
  %
  \cref{thm:transport-path}
  & 628-g1bd8602
  & The sentence preceding the theorem suggests that it follows from \cref{cor:transport-path-prepost,thm:transport-compose}, but actually it requires a separate path induction.\\
  %
  \cref{thm:transport-path}
  & 704-g70c069e
  & The sentence after the theorem should say that $\apfunc{(x \mapsto c)}$ is $p \mapsto\refl{c}$, not $\refl{c}$.\\
  %
  \cref{thm:transport-path2}
  & 364-g3c47534
  & The right-hand side of the displayed equality should be $\opp{(\apdfunc{f}(p))} \ct \apfunc{(\transfibf{B}{p})}(q) \ct \apdfunc{g}(p)$.\\
  %
  \cref{sec:compute-coprod}
  & 101-g645f763
  & In \cref{thm:path-coprod} and the preceding paragraph, in the equivalence $\eqv{(\inl(a)=x)}{\code(x)}$, the variable $a$ should be $a_0$. \\
  %
  \cref{sec:compute-coprod}
  & 370-g114db82
  & In the two displays after the proof of \cref{thm:path-coprod}, the terms should be $\encode(\inl(a), {\blank})$ and $\encode(\inr(b), {\blank})$.\\
  %
  \cref{sec:equality-semigroups}
  & 261-g4ccda0a
  & In the first displayed pair of equations, the type of $p_2$ should be $\transfib{\semigroupstrsym}{p_1}{(m,a)} = {(m',a')}$.\\
  %
  \cref{sec:equality-semigroups}
  & 402-g2297ecb
  & The right hand side of the last displayed equation should be $m'(e(x_1),e(x_2))$.\\
  %
  \cref{sec:universal-properties}
  & 305-g64685f1
  & In the discussion of universal properties for product types and $\Sigma$-types surrounding \cref{eq:sigma-lump}, the phrases ``left-to-right'' and ``right-to-left'' should be switched.\\
  %
  \cref{cha:basics} Notes
  & 379-ga57eab2
  & It should be mentioned that Hofmann and Streicher (1998) proposed an axiom similar to univalence, which is correct (and equivalent to univalence) for a universe of 1-types.\\
  %
  % Chapter 3
  %
  \cref{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.\\
  %
  \cref{thm:retract-contr}
  & 95-gce0131f
  & In the proof, $p$ should be $r$ to match the preceding definition of retraction.\\
  %
  % Chapter 4
  %
  \cref{lem:qinv-autohtpy}
  & 87-g693e9b9
  & At the end of the proof, \cref{thm:contr-paths} should be cited as the reason why $\sm{g:A\to A} (g = \idfunc[A])$ is contractible.\\
  %
  \cref{thm:equiv-iso-adj}
  & 275-g8ea9f71
  & In the proof, the path concatenations in the definitions of $\epsilon'$ and $\tau$ were written in reverse order.\\
  %
  \cref{thm:equiv-iso-adj}
  & 1043-gcfce4d7
  & In the proof, the type of $\tau(a)$ should be $\ap{f}{\eta(a)}=\opp{\epsilon(f(g(f(a))))}\ct (\ap{f}{\eta(g(f(a)))}\ct \epsilon(f(a)))$, instead of $\opp{\epsilon(f(g(f(a))))}\ct (\ap{f}{\eta(g(f(a)))}\ct \epsilon(f(a)))=\ap{f}{\eta(a)}$.\\
  %
  \cref{lem:coh-hprop}
  & 296-ge3dc076
  & In the proof, $\id[\hfib{f}{fx}]{(fgx,\epsilon(fx))}{(x,\refl{fx})}$ should be $\id[\hfib{f}{fx}]{(gfx,\epsilon(fx))}{(x,\refl{fx})}$.\\
  %
  \cref{thm:equiv-biinv-isequiv}
  & 272-gfd47093
  & At the end of the proof, the equivalence follows from the fact that $\ishae(f)$, not $\iscontr(f)$, is a mere proposition. \\
  %
  \cref{thm:lequiv-contr-hae}
  & 299-g85b729b
  & In the proof, $\lcoh{f}{g}{\epsilon}$ should be $\rcoh{f}{g}{\epsilon}$, and the final displayed equation should have $\proj{2}$ applied to both occurrences of $P(fx)$.\\
  %
  \cref{lem:func_retract_to_fiber_retract}
  & 265-g64000fb
  & The path concatenations in the definitions of $\varphi_b$ and $\psi_b$ (and subsequent equations) are reversed, and each $f(a)$ in the next two displayed equations should be $g(a)$.\\
  %
  \cref{fibwise-fiber-total-fiber-equiv}
  & 275-g84ab032
  & The first equivalence in the proof is not by~\eqref{eq:sigma-lump} but by \cref{ex:sigma-assoc}.\\
  %
  \cref{fibwise-fiber-total-fiber-equiv}
  & 202-g775a3f0
  & The last equivalence in the proof is not by~\eqref{eq:path-lump} but by \cref{thm:omit-contr,thm:contr-paths,ex:sigma-assoc}.\\
  %
  \cref{thm:nobject-classifier-appetizer}
  & 205-gf9fe386
  & In the proof, $e\cdot \proj1$ should be $\trans{(\ua(e))}{\proj1}$.  Also, explain its computation better.\\
  %
  \cref{sec:univalence-implies-funext}
  & 114-gaba76c8
  & The point of \cref{UA-eqv-hom-eqv} is that it follows from univalence without assuming function extensionality separately.\\
  %
  \cref{contrfamtotalpostcompequiv}
  & 484-g2ce1249
  & In the statement, ``precomposition'' should be ``post-composition''.\\
  %
  \cref{uatowfe}
  & 746-g4d540d6
  & In the definition of $\psi$ in the proof, transport has to be along $\happly(p,x)$ instead of along $p$.\\
  %
  \cref{ex:symmetric-equiv}
  & 358-g9543064
  & The text should be ``Show that for any $A,B:\UU$, the following type is equivalent to $\eqv A B$.  Can you extract from this a definition of a type satisfying the three desiderata of $\isequiv(f)$?''\\
  %
  % Chapter 5
  %
  \cref{sec:appetizer-univalence}
  & 706-ged2c765
  & In the proof that $\eqv{\nat}{\natp}$, the definitions of $f$ and $g$ should be $\rec\nat(\natp, \; \zerop, \;  \lamu{n:\nat} \sucp)$ and $\rec\natp(\nat, \; 0, \;  \lamu{n:\natp} \suc)$ respectively.\\
  %
  \cref{sec:w-types}
  & 125-g433f87e
  & In the definition of $\natw$, use $\bfalse$ for $0$ and $\btrue$ for $\suc$, to match the ordering of $\bfalse$ and $\btrue$ in \cref{sec:type-booleans}.\\
  %
  \cref{sec:w-types}
  & 551-g82b74bf
  & The definitions of $\natw$ and $\lst A$ as $\w$-types should be $\wtype{b:\bool} \rec\bool(\bbU,\emptyt,\unit,b)$ and $\wtype{x: \unit + A} \rec{\unit + A}(\bbU,  \emptyt,  \lamu{a:A} \unit, x)$.\\
  %
  \cref{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)$.\\
  %
  \cref{sec:w-types}
  & 525-gb1957b8
  & In the computation rule, the recursive call to $\rec{}$ is missing an argument.
  It should read $\rec{\wtype{x:A} B(x)}(E,e,\supp(a,f)) \jdeq e(a,f,\big(\lamu{b:B(a)} \rec{\wtype{x:A} B(x)}(E,e,f(b))\big))$.\\
  %
  \cref{sec:w-types}
  & 570-g6ec04c3
  & In the verification that $\dbl$ computes as expected, $e_t$ should be $e_0$ and $e_f$ should be $e_1$.\\
  %
  \cref{sec:initial-alg}
  & 554-g9b2a34b
  & The definition of the type of $\w$-homomorphisms (just before \cref{thm:w-hinit}) should read $\whom_{A,B}((C, s_C),(D,s_D)) \defeq \sm{f : C \to D} \prd{a:A}{h:B(a)\to C} \id{f(s_C(a,h))}{s_D(a, f\circ h)}$.\\
  %
  \cref{sec:htpy-inductive}
  & 917-gd6960ad
  & In the first paragraph, the definition of $\natw$ should be $\wtype{b:\bool} \rec\bool(\bbU,\emptyt,\unit,b)$.\\
  %
  \cref{sec:htpy-inductive}
  & 608-g6af101f
  & In the computation rule for homotopy $\w$-types, the left-hand side should be $\rec{\wtypeh{x:A} B(x)}(E,e,\supp(a,f))$.\\
  %
  \cref{eq:example-comp}
  & 912-g04d3fb6
  & In the preceeding sentence, $\delta:d$ should be $\delta:D$.\\
  %
  \cref{sec:generalizations}
  & 908-g4b2eb10
  & The second two constructors of $\mathsf{paritynat}$ should be $\mathsf{esucc} : \mathsf{paritynat}(\btrue) \to \mathsf{paritynat}(\bfalse)$ and $\mathsf{osucc} : \mathsf{paritynat}(\bfalse) \to \mathsf{paritynat}(\btrue)$.\\
  %
  \cref{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$.\\
  %
  \cref{ex:same-recurrence-not-defeq}
  & 622-ga0bd007
  & The two functions should satisfy the same recurrence judgmentally.\\
  %
  \cref{ex:one-function-two-recurrences}
  & 622-ga0bd007
  & The function should satisfy both recurrences judgmentally.\\
  %
  % Chapter 6
  %
  \cref{sec:dependent-paths}
  & 54-gd4a47c2
  & Soon after \cref{rmk:defid}, the phrase ``An element $b:P(\base)$ in the fiber over the constructor $\base:\nat$'' should say $\base:\Sn^1$.\\
  %
  \cref{thm:uniqueness-for-functions-on-S1}
  & 423-gf763ae1
  & \cref{thm:transport-path,thm:dpath-path} are needed to put $q$ in the form required by the induction principle.\\
  %
  \cref{thm:interval-funext}
  & 417-g4aa6a15
  & Added \cref{ex:funext-from-interval}: the function constructed in \cref{thm:interval-funext} is actually an inverse to $\happly$, so that the full function extensionality axiom follows from an interval type.\\
  %
  \cref{thm:S1-autohtpy}
  & 625-g950efa9
  & In the second paragraph of the proof, the appeal to function extensionality should be omitted.\\
  %
  \cref{sec:circle}
  & 327-g7cbe31c
  & In the first sentence after the proof of \cref{thm:apd2}, ``$P:\Sn^2\to P$'' should be ``$P:\Sn^2\to\type$''.\\
  %
  \cref{sec:circle}
  & 1039-g30da4c6
  & In the sentence after the proof of \cref{thm:apd2}, the type family in which $s$ is a dependent path should be $\lam{p} \dpath P p b b$ instead of $P$.\\
  %
  \cref{sec:cell-complexes}
  & 289-gdefeb8c
  & In the induction principle for the torus, the types of $p'$ and $q'$ should be $\dpath P p {b'} {b'}$ and $\dpath P q b b$ respectively.\\
  %
  \cref{sec:hubs-spokes}
  & 289-gdefeb8c
  & In the induction principle for the torus, the types of $p'$ and $q'$ should be $\dpath P p {b'} {b'}$ and $\dpath P q b b$ respectively.\\
  %
  \cref{sec:hittruncations}
  & 468-g5472874
  & The induction principle for $\brck{A}$ should conclude $f(\bproj a)\jdeq g(a)$, not $f(\bproj a)\jdeq a$.  And in the hypotheses of the induction principle for $\trunc0 A$ and in the proof of \cref{thm:trunc0-ind}, $v:\dpath{B}{u(x,y,p,q)}{p}{q}$ should instead be $v:\dpath{B}{u(x,y,p,q)}{r}{s}$.\\
  %
  \cref{sec:hittruncations}
  & 860-gc7d862c
  & In the penultimate paragraph, the ``unobjectionable'' constructor for $\trunc0 A$ should begin ``For every $f:S\to \trunc0 A$'', not ``For every $f:S\to A$''.\\
  %
  \cref{thm:quotient-ump}
  & 961-gde36592
  & The first sentence of the second paragraph of the proof should end with $g(x) = \overline{g\circ q}(x)$.\\
  %
  \cref{lem:quotient-when-canonical-representatives}
  & 514-g18ade45
  & Instead of ``is the set-quotient of $A$ by $\eqr$'', the statement should say ``satisfies the universal property of the set-quotient of $A$ by~$\eqr$, and hence is equivalent to it''.
  In the proof, the second displayed equation should be $e'(g, s) (x,p) \defeq g(x)$.
  The fourth displayed equation should be $e(e'(g, s)) \jdeq e(g \circ \proj{1}) \jdeq (g \circ \proj{1} \circ q, {\nameless})$, the fifth should be $g(\proj{1}(q(x))) \jdeq g(r(x)) = g(x)$, and the proof should conclude with ``$g$ respects $\eqr$ by the assumption $s$''.\\
  %
  \cref{thm:sign-induction}
  & 535-g0a9abfe
  & The ``computation rules'' satisfied by $f$ are only propositional equalities.
  Also, the proof requires transport across a few unmentioned equivalences.\\
  %
  \cref{thm:looptothe}
  & 535-g0a9abfe
  & The defining clauses should use $\defid$ rather than $\defeq$ (see the erratum for \cref{thm:sign-induction}).
  Also, the first clause should say $\refl{a}$ rather than $\refl{\base}$.\\
  %
  \cref{thm:transport-is-given}
  & 682-g3af5dbe
  & Three occurrences of $P$ in the statement should be $B$.\\
  %
  \cref{thm:flattening-cp}
  & 457-g411ec6d
  & The right-hand side of the displayed equation in the proof should be $(\cc(g(b)),D(b)(y))$.\\
  %
  \cref{thm:flattening-cp}
  & 961-gde36592
  & After the display we should have $\pp(b):\cc(f(b))=\cc(g(b))$.\\
  %
  \cref{sec:flattening}
  & 519-gc99a54c
  & $f$ denotes a map $B\to A$ in this section and should not be re-used for functions defined by induction on $\sm{w:W} P(w)$; we may use $k$ instead.
  Thus $f$ should be $k$ in the last sentence of \cref{thm:flattening-rect}; the first sentence of its proof; the second and third sentences of the paragraph after its proof; the last sentence of \cref{thm:flattening-rectnd}; the first, second, and last sentences of its proof; throughout the statement and proof of \cref{thm:ap-sigma-rect-path-pair}; the statement of \cref{thm:flattening-rectnd-beta-ppt}; and the second sentence of its proof.\\
  %
  \cref{thm:flattening-rect}
  & 537-gdf3b51d
  & In the display after the definition of $q$, the transport in the first line should be with respect to $x\mapsto Q(\cct'(g(b),x))$, and in the second line the subscript of $\apfunc{}$ should be $x\mapsto \cct'(g(b),x)$.\\
  %
  \cref{thm:flattening-rect}
  & 961-gde36592
  & The subscript of $\apfunc{}$ should also be $x\mapsto \cct'(g(b),x)$ in the third, fourth, and fifth displays.
  In the fourth and fifth displays, the path-concatenations should be in the other order.
  And in the fifth display, $\refl{g(b)}$ should be $\refl{\cc(g(b))}$.\\
  %
  \cref{thm:ap-sigma-rect-path-pair}
  & 501-ge895f81
  & Both occurrences of $P$ in the statement should be $Y$, and both occurrences of $Q$ in the proof should be $Z$.\\
  %
  % Chapter 7
  %
  \cref{thm:h-level-retracts}
  & 180-gb672a4d
  & In the last displayed equation of the proof, $q$ should be $r$.\\
  %
  \cref{thm:isaprop-isofhlevel}
  & 101-g713f48c
  & The base case in the proof is just \cref{thm:isprop-iscontr}.\\
  %
  \cref{sec:truncations}
  & 480-gdc84050
  & The third paragraph is wrong: in contrast to \cref{rmk:spokes-no-hub}, it \emph{would} actually work to define $\trunc nA$ omitting the hub point.\\
  %
  \cref{lem:hedberg-helper}
  & 644-g627c0a8
  & In the proof of the lemma, ``If $x$ is $\inr(f)$'' should be ``If $x$ is $\inr(t)$''.\\
  %
  \cref{thm:path-truncation}
  & 412-gb9582fc
  & In the proof, \encode and \decode should be switched.\\
  %
  \cref{lem:nconnected_postcomp_variation}
  & 801-g01922a8
  & The converse direction is false unless $Q$ is fiberwise merely inhabited.  Also, the occurrences of $\ap f p$ and $\ap f {\proj 2 w}$ in the proof should be just $p$ and $\proj 2 w$, respectively.\\
  %
  \cref{lem:connected-map-equiv-truncation}
  & 367-g1c8c07e
  & In the proof that the first composite is the identity, all occurrences of $y$ should be $f(x)$.\\
  %
  \cref{thm:modal-char}
  & 658-g016f3a4
  & In the second paragraph of the proof, the first two occurrences of $\proj2$ (but not the third) should be $\proj1$.\\
  %
  \cref{ex:s2-colim-unit}
  & 101-ga366be2
  & ``entires'' should be ``entirely''.\\
  %
  \cref{ex:s2-colim-unit}
  & 683-g8941e50
  & This exercise needs more precise definitions of ``diagram'' and ``colimit''.\\
  %
  \cref{ex:acnm}
  & 1074-gcd42187
  & $\choice{\infty,\infty}$ is not \cref{thm:ttac}, but the identity function.\\
  %
  \cref{ex:acnm}
  & 603-ge113e08
  & The penultimate sentence should ask ``Is $\choice{n,m}$ consistent with univalence for any $m\ge 0$ and any $n$?''.\\
  %
  % Chapter 8
  %
  \cref{lem:s1-encode-decode}
  & 535-g0a9abfe
  & The proof by induction on $n:\Z$ is justified by \cref{thm:sign-induction}, not \cref{thm:looptothe}.\\
  %
  \cref{thm:iscontr-s1cover}
  & 535-g0a9abfe
  & The clauses defining $q_z$ should use $\defid$ rather than $\defeq$ (see the erratum for \cref{thm:sign-induction}).\\
  %
  \cref{thm:suspension-increases-connectedness}
  & 1062-gf3bfeae
  & In the proof, $E$ is not $(n + 1)$-connected but $(n + 1)$-truncated.\\
  %
  \cref{thm:conn-pik}
  & 1023-gf188aeb
  & The proof requires a separate argument for $k=0$.\\
  %
  \cref{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 \cref{ex:HopfJr,ex:SuperHopf}.\\
  %
  \cref{lem:fibration-over-pushout}
  & 1062-gf3bfeae
  & In the definition of ${E^{\mathrm{tot}}}'$ in the proof, $e_C$ should be $e_X$.\\
  %
  \cref{thm:conn-trunc-variable-ind}
  & 396-g868335b
  & In the proof, the function $k$ should have type $\prd{a:A} P(f(a))$.
  It should also be named $\ell$, to avoid confusion with the integer $k$.\\
  %
  \cref{thm:freudcode}
  & 87-g3f977b2
  & In the second displayed equation in the proof, $\merid(x_1)$ should be $\opp{\merid(x_1)}$.\\
  %
  \cref{thm:wedge-connectivity}
  & 399-g8897c94
  & In the last sentence of the proof, ``$(n-1)$-connected'' should be ``$(n-1)$-truncated''.\\
  %
  \cref{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}$''.\\
  %
  \cref{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}$.\\
  %
  \cref{sec:freudenthal}
  & 474-g5289470
  & $\pi_3(\Sn^2)=\Z$ should be stated as \cref{thm:pi3s2}, following from \cref{cor:pis2-hopf,thm:pinsn}.\\
  %
  \cref{thm:whiteheadn}
  & 1092-ge3b8b71
  & After applying the induction hypothesis, it additionally needs to be checked that for every path $p : a = a$ the map $\pi_k(\apfunc f):\pi_k(x = x,p) \to \pi_k(f(x) = f(x),\apfunc f(p))$ is a bijection. \\
  %
  % Chapter 9
  %
  \cref{ct:functor}
  & 807-gebec78b
  & In \cref{ct:functor:comp}, it should read ``$\hom_A(b,c)$'' instead of ``$\hom_B(b,c)$''.\\
  %
  \cref{ct:yoneda}
  & 971-g6096085
  & The sequence of equations at the end of the proof should begin with $\alpha_{a'}(f) = \alpha_{a'} (\y a_{a,a'}(f)(1_a))$, and thereafter the subscripts should remain $a,a'$ rather than $a',a$.\\
  %
  \cref{ct:sig}
  & 897-g94fb722
  & In~\ref{item:sigcmp}, ``if $f:\hom_X(x,y)$'' should be ``if $f:\hom_X(x,y)$ and $g:\hom_X(y,z)$''.\\
  %
  \cref{sec:sip}
  & 1111-g3332a31
  & The type of objects $A_0$ of the precategory $A$ of $(P,H)$-structures should be defined as $\sm{x:X_0} Px$, not $\sm{x:X} Px$.\\
  %
  \cref{cha:category-theory}
  & 966-g04374f5
  & The first sentence after \cref{ct:cat-weq-eq} should begin ``Therefore, if a precategory $A$ admits a weak equivalence functor $A\to \widehat{A}$ \emph{into a category}\dots''.\\
  %
  \cref{thm:rezk-completion}
  & 313-g8ee79db
  & In the second proof, the third constructor of $\widehat A_0$ is unneeded; it follows from the fourth constructor and path induction.
  In the fifth constructor, $j(g)\ct j(f)$ should be $j(f)\ct j(g)$, and similarly throughout the proof.
  Finally, for consistency, the 1-truncation constructor should be included explicitly (this was intended to be implied by "higher inductive 1-type").\\
  %
  \cref{cha:category-theory} Notes
  & 379-ga57eab2
  & It should be mentioned that Hofmann and Streicher (1998) also considered this definition of category.\\
  %
  % Chapter 10
  %
  \cref{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$''.\\
  %
  \cref{thm:ordunion}
  & 140-gd7f8960
  & The statement should say $X:\UU$ rather than $X:\UU_\UU$.\\
  %
  \cref{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$''.\\
  %
  \cref{thm:wop}
  & 871-g85bcd11
  & The statement of~\ref{item:wop1} should end with $Y:\powerp X$, not $Y:\power X$.\\
  %
  \cref{sec:cumulative-hierarchy}
  & 753-gc87ce23
  & The second clause in the induction principle for $V$ should say ``Verify that if $f : A \to V$ and $g : B \to V$ satisfy~\eqref{eq:V-path}, then $\dpath{P}{q}{h(\vset(A,f))}{h(\vset(B,g))}$, where $q$ is the path arising from the second constructor of $V$ and~\eqref{eq:V-path}, assuming inductively that $\dpath{P}{p}{h(f(a))}{h(g(b))}$ whenever $p:f(a)=g(b)$.''\\
  %
  \cref{sec:cumulative-hierarchy}
  & 706-ged2c765
  & The proof that membership is well-defined should end with ``hence $x = g(b)$ and $x \in \vset(B,g)$.''\\
  %
  \cref{sec:cumulative-hierarchy}
  & 1056-g4060c2b
  & In the definition of $V$-set, the notation $v \in V$ should be $v:V$.\\
  %
  \cref{thm:VisCST}
  & 708-g6f53189
  & In the pairing axiom, the pair class should be denoted $\{u, v\}$, not $u\cup v$.\\
  %
  \cref{thm:VisCST}
  & 723-g9cf5b44
  & The replacement axiom should be given $x : V$ (not $a : V$) and the displayed class should be $\setof{ y | \exis{z : V} z \in x \land y = r(z)}$.
  Its proof should begin ``let $C$ denote the class in question.''\\
  %
  \cref{thm:VisCST}
  & 706-ged2c765
  & In the proof of the function set axiom, ``the types of elements $[u] \mono V$ and $[u] \mono V$'' should be ``the types of members $[u] \mono V$ and $[v] \mono V$.''\\
  %
  \cref{ex:strong-collection}
  & 1053-ge13dd65
  & Extra parentheses around $\fall{x\in v}\exis{y} R(x,y)$ are needed to make the formula unambiguous.\\
  %
  \cref{ex:choice-cumulative-hierarchy-choice}
  & 1053-ge13dd65
  & Extra parentheses around $\fall{y\in x}\exis{z\in V} z\in y$ are needed to make the formula unambiguous.\\
  %
  \cref{ex:choice-cumulative-hierarchy-choice}
  & 1056-g4060c2b
  & The notation $\in V$ should be $:V$.\\
  %
  % Chapter 11
  %
  \cref{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)$''.\\
  %
  \cref{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$''.\\
  %
  \cref{sec:RD-cauchy-complete}
  & 832-g0cb658e
  & In the second paragraph, at ``From this we get'', the universal quantification should be over~$\delta$ as well.\\
  %
  \cref{defn:RC-approx}
  & 1069-g3b333d5
  & In the description of openness of $\approx$, ``$\exis{\epsilon : \Qp}$'' should be ``$\exis{\delta : \Qp}$''.\\
  %
  \cref{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)$.\\
  %
  \cref{eg:surreal-addition}
  & 636-g827e7ea
  & In the first bullet point, to prove $x^L+z < x+z$ requires a $\NO$-induction on $z$, since only when $z$ is defined by a cut can we say that $x^L+z$ is a left option of $x+z$.\\
  %
  \cref{ex:mean-value-theorem}
  & 222-g3453cf1
  & This is the intermediate value theorem, not the mean value theorem.\\
  %
  \cref{eg:surreal-addition}
  & 980-ge9d0398
  & For the codomain of the outer recursion, the conditions should be $(x<y) \to (g(x)<g(y))$ and $(x\le y) \to (g(x)\le g(y))$.  In the first bullet of the verification that inequalities are preserved, the outer inductive hypotheses give non-strict inequalities $x^L+y \le x^L+z$ and $x^R+ y \le x^R+z$, and no additional $\NO$-induction on $z$ is required (it is already known to be defined by a cut).\\
  %
  \cref{eg:surreal-addition}
  & 980-ge9d0398
  & The verification that Conway's definition of $x+y$ is a surreal number (i.e.\ all its left options are $<$ all its right options) was omitted.  This requires turning the inner recursion into an inner induction with codomain a varying subset of $\NO$, as in \cref{defn:No-codes}.\\
  %
  % Appendix A
  %
  \cref{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''.\\
  %
  \cref{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.\\
  %
  \cref{sec:more-formal-sigma}
  & 26-gcd691e8
  & In $\Sigma$-\rcomp\ and the following paragraph, $y.C$ should be $z.C$, and ``we bind \dots $y$ in $C$'' should likewise say $z$.\\
  %
  \cref{sec:more-formal-unit}
  & 338-g4e1c688
  & The $c$ argument in the eliminator for $\unit$ (in the $\unit$-\relim\ and $\unit$-\rcomp\ rules) should not bind a variable of type $\unit$.\\
  %
  \cref{sec:more-formal-identity}
  & 578-ga4b94a5
  & The unbased eliminator for the identity type should be named $\indid{A}$, not $\indidb{A}$.\\
%% END ERRATA
\end{longtable}

\end{document}