minor

intro-uf.tex

@@ -3294,7 +3294,7 @@ \section{Predicates and subtypes}
 Note the slight subtlety of this definition together with
 \cref{def:decidability}: Any proposition has decidable identity types
 (since each instance is contractible) and is thus a \emph{decidable set},
-even though it may not be a \emph{decidable as a proposition}.
+even though it may not be \emph{decidable as a proposition}.
 
 The way we phrased this definition implies that $A$ is a set.
 The following celebrated and useful theorem states that this is unnecessary.
@@ -4127,7 +4127,7 @@ \section{The type of finite sets}
 that $\UU_0$ is the smallest universe.
 
 \begin{xca}\label{xca:finsets-decidable}
-Show that every finite set has decidable equality.
+Show that every finite set is a decidable set.
 \end{xca}
 
 We have already seen several examples of 2-element sets:
@@ -4144,7 +4144,7 @@ \section{The type of finite sets}
 an \emph{arbitrary} 2-element set with any of these.
 The following exercise makes this precise, and gives a
 useful and surprising case of a 2-element set
-that actually \emph{can} be identified.
+that actually \emph{can} be identified with $\bn{2}$.
 
 \begin{xca}\label{xca:2-element-sets}
 Show that $T\eqto T$ is a 2-element set for every 2-element set $T$.