-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy patherrata.tex
167 lines (133 loc) · 5.08 KB
/
errata.tex
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
% 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{\textsc{\scriptsize \textcolor{gray}{[Draft of \today]}}}
\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}
\title{Errata for the HoTT Book, first edition}
\begin{document}
\maketitle
\begin{tabular}{llp{11cm}}
\textbf{Location} & \textbf{Fixed in} & \textbf{Change}\\
\hline
\autoref{sec:sigma-types}
& be277a8
& 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:more-formal-sigma}
& cd691e8
& In $\Sigma$-\comp\ and the following paragraph, $y.C$ should be $z.C$, and ``we bind \dots $y$ in $C$'' should likewise say $z$.\\
\autoref{sec:coproduct-types}
& 264d934
& In two displayed equations, $f(\inl(b))$ should be $f(\inr(b))$.\\
\autoref{sec:sigma-types}
& d0bfa0d
& At two places in the definition of $\ac$, $R(a,\fst(g(x)))$ should be $R(x,\fst(g(x)))$.\\
\autoref{sec:dependent-paths}
& d4a47c2
& 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$.\\
\end{tabular}
\end{document}