Move the counterexample to an exercise

Author: jeanas

basics.tex

@@ -1414,11 +1414,10 @@ \section{\texorpdfstring{$\Sigma$}{Σ}-types}
 \index{total!space}%
 Thus, we are saying that a path $w=w'$ in the total space determines (and is determined by) a path $p:\proj1(w)=\proj1(w')$ in $A$ together with a path from $\proj2(w)$ to $\proj2(w')$ lying over $p$, which seems sensible.
 
-\begin{rmk}
-  Note that if we have $x:A$ and $u,v:P(x)$ such that $(x,u)=(x,v)$, it does not follow that $u=v$.
+\begin{rmk}\label{rmk:sigma-equality-extraction}
+  Note that if we have $x:A$ and $u,v:P(x)$ such that $(x,u)=(x,v)$, it does not follow that $u=v$ --- see \cref{ex:sigma-eq-components-neq} for a counterexample.
   All we can conclude is that there exists $p:x=x$ such that $\trans p u = v$.
   This is a well-known source of confusion for newcomers to type theory, but it makes sense from a topological viewpoint: the existence of a path $(x,u)=(x,v)$ in the total space of a fibration between two points that happen to lie in the same fiber does not imply the existence of a path $u=v$ lying entirely \emph{within} that fiber.
-  For example, with univalence, we will be able to show $(\bool, \bfalse) =_{\sm{A:\type}A} (\bool, \btrue)$, although $\bfalse \neq_{\bool} \btrue$.
 \end{rmk}
 
 The next theorem states that we can also reverse this process.
@@ -2691,6 +2690,10 @@ \section{Universal properties}
   State and prove a version of \cref{lem:htpy-natural} for dependent functions.
 \end{ex}
 
+\begin{ex}\label{ex:sigma-eq-components-neq}
+  We have seen that $\bfalse \neq \btrue$ (\cref{rmk:false-neq-true}). Show that, nevertheless, $(\bool, \bfalse) =_{\sm{A:\type}A} (\bool, \btrue)$ (see \cref{rmk:sigma-equality-extraction}).
+\end{ex}
+
 % Local Variables:
 % TeX-master: "hott-online"
 % End: