@@ -29,6 +29,34 @@ twoPlusTwo = refl
2929\end{SaveVerbatim}
3030\useverb{eqprf}
3131
32+\subsection{The Empty Type}
33+
34+There is an empty type, \texttt{\_|\_}, which has no constructors. It is
35+therefore impossible to construct an element of the empty type, at least
36+without using a partially defined or general recursive function (see Section
37+\ref{sect:totality} for more details). We can therefore use the empty type
38+to prove that something is impossible, for example zero is never equal
39+to a successor:
40+
41+\begin{SaveVerbatim}{natdisjoint}
42+
43+imp : (n : Nat) -> O = S n -> _|_
44+imp n p = replace {P = impTy} p ()
45+ where
46+ impTy : Nat -> Set
47+ impTy O = ()
48+ impTy (S k) = _|_
49+
50+\end{SaveVerbatim}
51+\useverb{natdisjoint}
52+
53+\noindent
54+There is no need to worry too much about how this function works --- essentially,
55+it applies the library function \texttt{replace}, which uses an equality proof to
56+transform a predicate. Here we use it to transform a value of a type which can exist,
57+the empty tuple, to a value of a type which can't, by using a proof of something
58+which can't exist.
59+
3260\subsection{Simple Theorems}
3361
3462When type checking dependent types, the type itself gets \emph{normalised}. So imagine