xca:2-element-sets

group.tex

@@ -2014,7 +2014,7 @@ \section{Infinity groups (\texorpdfstring{\inftygps}{∞-groups})}
   $\Aut_\UU(S)$ is an ordinary group.
 
   Because we have an inclusion $\UUp^{=1} \hookrightarrow \UUp^{>0}$,
-  we get a corresponding inclusion $\Group \hookrightarrow \typeinftygp$.
+  we get a corresponding injection $\Group \hookrightarrow \typeinftygp$.
 \end{remark}
 
 \begin{definition}

intro-uf.tex

@@ -4101,7 +4101,9 @@ \section{The type of finite sets}
   Hence we also have $\FinSet_n
   \jdeq \Set_{(\bn{n})} \eqto \FinSet_{(\bn{n})}
  \eqto \UU_{(\bn{n})}$.}
-as $\bn{n}$ we say that \emph{$S$ has cardinality $n$} or that \emph{the cardinality of $S$ is $n$}.
+as $\bn{n}$ we say that \emph{$S$ has cardinality $n$}, 
+or that \emph{the cardinality of $S$ is $n$}, 
+or that $S$ \emph{is an $n$-element set}.
 
 \begin{definition}\label{def:groupoidFin}
 The \emph{groupoid of finite sets} is defined by
@@ -4127,6 +4129,33 @@ \section{The type of finite sets}
 \cref{sec:natural-numbers}, and our assumption
 that $\UU_0$ is the smallest universe.
 
+\begin{xca}\label{xca:finsets-decidable}
+Show that every finite set has decidable equality.
+\end{xca}
+
+We have already seen several examples of 2-element sets:
+$\bool$, $\bn{2}$, $\bn{1}\amalg\bn{1}$ that can easily
+be identified. Which one to use
+depends on the context and is a matter of convenience.
+Later we will also use $\set{\pm1}$. In contrast
+to these concrete examples, one cannot identify\footnote{%
+Any 2-element set is by definition \emph{merely} identified
+with $\bn{2}$, but the problem is that we cannot ''name''
+the elements, not even one of them. Having a name for one
+of the elements would be sufficient, since then the ''other''
+element is uniquely determined.}
+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.
+
+\begin{xca}\label{xca:2-element-sets}
+Show that $T\eqto T$ is a 2-element set for every 2-element set $T$.
+Using univalence, show that $\neg\prod_{T:\FinSet_2}(T\eqto\bn{2})$.
+In spite of the above, give an element of
+$\prod_{T:\FinSet_2}((T\eqto T)\eqto\bn{2})$.
+\end{xca}
+
 \section{Type families and maps}
 \label{sec:typefam}