You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Copy file name to clipboardExpand all lines: errata.tex
+2-2Lines changed: 2 additions & 2 deletions
Original file line number
Diff line number
Diff line change
@@ -234,7 +234,7 @@
234
234
& Emphasize that path induction, like all other induction principles, defines a \emph{specified} function.\\
235
235
%
236
236
\cref{sec:identity-types}
237
-
& % merge of f44ef3b
237
+
& 1373-g142de42
238
238
& In the second proof that based path induction implies path induction, the observation should be that $f$ can be obtained as an instance of $\indid{A}$, not $\indidb{A}$.\\
239
239
%
240
240
\cref{sec:identity-types}
@@ -810,7 +810,7 @@
810
810
% Chapter 10
811
811
%
812
812
\cref{card:semiring}
813
-
& % merge of 8297933c
813
+
& 1303-ga530d97
814
814
& The equation $\cd{B}\times\cd{A} \jdeq\cd{B\times A}$ in the proof should be $\cd{B}\cdot\cd{A} \jdeq\cd{B\times A}$.\\
0 commit comments