Skip to content

Commit a1e06c4

Browse files
authored
Merge pull request HoTT#1180 from enklht/typos
fix: Comment out merge sign in errata.tex
2 parents 9dd4992 + 1763fc2 commit a1e06c4

File tree

1 file changed

+5
-5
lines changed

1 file changed

+5
-5
lines changed

errata.tex

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -411,7 +411,7 @@
411411
%
412412
\cref{subsec:logic-hprop}
413413
& 37-g0bd66c8
414-
& In the discussion for $\Sigma$-types in the last paragraph, $A$ is an arbitrary type.
414+
& In the discussion for $\Sigma$-types in the last paragraph, $A$ is an arbitrary type.\\
415415
%
416416
\cref{thm:retract-contr}
417417
& 95-gce0131f
@@ -480,12 +480,12 @@
480480
& 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)$?''\\
481481
%
482482
\cref{thm:object-classifier}
483-
& merge of 367864df
484-
& To maintain consistency, one line was added at the end of the computation of the composite equivalence in the proof.
483+
& % merge of 367864df
484+
& To maintain consistency, one line was added at the end of the computation of the composite equivalence in the proof.\\
485485
%
486486
\cref{thm:fiber-of-a-fibration}
487-
& merge of edb908a2
488-
& The type of $\proj{1}$ should be $(\sm{x:A}P(x))\to A$.
487+
& % merge of edb908a2
488+
& The type of $\proj{1}$ should be $(\sm{x:A}P(x))\to A$.\\
489489
%
490490
% Chapter 5
491491
%

0 commit comments

Comments
 (0)