exercises: add solution to disjoint-or

Author: langston-barrett

exercise_solutions.tex

@@ -342,8 +342,8 @@ \subsection*{Solution to \cref{ex:prop-endocontr}}
 
 \subsection*{Solution to \cref{ex:lem-mereprop}}
 
-Let $h:\isprop(A)$, and let $x,y:A+(\neg A)$. We want to show that $x=y$.
-We proceed by cases using the induction principle for coproducts.
+Assume $A$ is a proposition, and let $x,y:A+(\neg A)$. We want to show that
+$x=y$. We proceed by cases using the induction principle for coproducts.
 \begin{enumerate}
   \item Assume $x\jdeq \inl(a)$ and $y\jdeq \inr(n)$. Then
     $n(a):\emptyt$ gives us a contradiction.
@@ -362,6 +362,24 @@ \subsection*{Solution to \cref{ex:lem-mereprop}}
     $\id[]{n_1}{n_2}$.
 \end{enumerate}
 
+\subsection*{Solution to \cref{ex:disjoint-or}}
+
+Assume $h:\neg(A\times B)$, and let $x,y:A+B$. We want to show that
+$x=y$. We proceed by cases using the induction principle for coproducts.
+\begin{enumerate}
+  \item Assume $x\jdeq \inl(a)$ and $y\jdeq \inr(b)$ for $a:A$ and $b:B$.
+    Then $h(a,b):\emptyt$, and we can use the destructor for $\emptyt$ to
+    conclude anything we wish.
+  \item Assume $x\jdeq \inr(b)$ and $y\jdeq \inl(a)$. Then $h(a,b):\emptyt$, and
+    we're done.
+  \item Assume $x\jdeq \inl(a_1)$ and $y\jdeq \inl(a_2)$. By the
+    characterization of paths in coproduct types (\cref{sec:compute-coprod}), we
+    know $\eqv{(\id[]xy)}{(\id[]{a_1}{a_2})}$, and we have $\id[]{a_1}{a_2}$
+    since $A$ is a proposition. 
+  \item Assume $x\jdeq \inr(b_1)$ and $y\jdeq \inr(b_2)$. Just as above,
+    we have $\eqv{(\id[]xy)}{(\id[]{b_1}{b_2})}$, and $\id[]{b_1}{b_2}$.
+\end{enumerate}
+
 \subsection*{Solution to \cref{ex:decidable-choice}}
 
 The hypotheses imply that