Merge pull request #1174 from enklht/typos

Fix Minor Typos in Proofs of Corollary 4.9.3 and Theorem 4.8.4

Author: mikeshulman

equivalences.tex

@@ -886,7 +886,8 @@ \section{The object classifier}
 \begin{align*}
 a & \mapsto \pairr{f(a),\; \pairr{a,\refl{f(a)}}}\\
 & \mapsto \pairr{f(a), \; \hfiber{f}{f(a)}, \; \refl{\hfiber{f}{f(a)}}, \; \pairr{a,\refl{f(a)}}}\\
-& \mapsto \pairr{f(a), \; \hfiber{f}{f(a)}, \; \pairr{a,\refl{f(a)}}, \; \refl{\hfiber{f}{f(a)}}}.
+& \mapsto \pairr{f(a), \; \hfiber{f}{f(a)}, \; \pairr{a,\refl{f(a)}}, \; \refl{\hfiber{f}{f(a)}}}\\
+& \mapsto \pairr{f(a), \; \pairr{\hfiber{f}{f(a)}, \; \pairr{a,\refl{f(a)}}}, \; \refl{\hfiber{f}{f(a)}}}.
 \end{align*}
 Therefore, we get homotopies $f\htpy\proj1\circ e$ and $\vartheta_f\htpy \proj2\circ e$.
 \end{proof}
@@ -944,7 +945,7 @@ \section{Univalence implies function extensionality}
 \end{cor}
 
 \begin{proof}
-  By \cref{thm:fiber-of-a-fibration}, for $\proj{1}:\sm{x:A}P(X)\to A$ and $x:A$ we have an equivalence
+  By \cref{thm:fiber-of-a-fibration}, for $\proj{1}:(\sm{x:A}P(x))\to A$ and $x:A$ we have an equivalence
   \begin{equation*}
     \eqv{\hfiber{\proj{1}}{x}}{P(x)}.
   \end{equation*}

errata.tex

@@ -479,6 +479,14 @@
   & 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)$?''\\
   %
+  \cref{thm:object-classifier}
+  & merge of 367864df
+  & To maintain consistency, one line was added at the end of the computation of the composite equivalence in the proof.
+  %
+  \cref{thm:fiber-of-a-fibration}
+  & merge of edb908a2
+  & The type of $\proj{1}$ should be $(\sm{x:A}P(x))\to A$.
+  %
   % Chapter 5
   %
   \cref{sec:appetizer-univalence}