+The introduction and elimination for $\top$ and $\lcbool$ are unsurprising.
+Note that in the $\lcite{\dotsb}{\dotsb}{\dotsb}$ construct the type of the
+branches are dependent on the value of the conditional.
+
+The rules for $\mathsf{W}$, on the other hand, are quite an eyesore. The idea
+behind $\mathsf{W}$ types is to build up `trees' where shape of the number of
+`children' of each node is dependent on the value in the node. This is
+captured by the $\lhd$ constructor, where the argument on the left is the value,
+and the argument on the right is a function that returns a child for each
+possible value of $\tyb[\text{node value}]$, if $\lcw{x}{\tya}{\tyb}$. The
+recursor $\lcrec{\termt}{x}{\tyc}{\termp}$ uses $p$ to inductively prove that
+$\tyc[\termt]$ holds.
+
+\subsection{Some examples}
+
+Now we can finally provide some meaningful examples. I will use some
+abbreviations and convenient syntax:
+\begin{itemize}
+ \item $\_\mathit{operator}\_$ to define infix operators
+ \item $\abs{\{x : \tya\}}{\dotsb}$ to define an abstraction that I will not
+ explicitly apply since the $x$ can be inferred easily.
+ \item $\abs{x\appspace y\appspace z : \tya}{\dotsb}$ to define multiple abstractions at the same
+ time
+ \item I will omit the explicit typing when forming $\exists$ or $\mathsf{W}$,
+ and when eliminating $\lcbool$, since the types are almost always clear and
+ writing them each time is extremely cumbersome.
+\end{itemize}
+
+\subsubsection{Sum types}
+
+We would like to recover our sum type, or disjunction, $\vee$. This is easily
+done with $\exists$:
+\begin{eqnarray*}
+ \_\vee\_ & = & \abs{\tya\appspace\tyb : \lcsetz}{\lcexists{x}{\lcbool}{\lcite{x}{\tya}{\tyb}}} \\
+ \lcinl & = & \abs{\{\tya\appspace\tyb : \lcsetz\}}{\abs{x : \tya \vee \tyb}{(\lctrue, x)}} \\
+ \lcinr & = & \abs{\{\tya\appspace\tyb : \lcsetz\}}{\abs{x : \tya \vee \tyb}{(\lcfalse, x)}} \\
+ \mathsf{case} & = & \abs{\{\tya\appspace\tyb\appspace\tyc : \lcsetz\}}{\abs{x : \tya \vee \tyb}{\abs{f : \tya \tyarr \tyc}{\abs{g : \tyb \tyarr \tyc}{ \\
+ & & \hspace{0.5cm} \app{(\lcited{\lcfst x}{b}{(\lcite{b}{A}{B}) \tyarr C}{f}{g})}{(\lcsnd x)}}}}}
+\end{eqnarray*}
+What is going on here? We are using $\exists$ with $\lcbool$ as a tag, so that
+we can choose between one of two types in the second element. In
+$\mathsf{case}$ we use $\lcite{\lcfst x}{\dotsb}{\dotsb}$ to discriminate on the
+tag, that is, the first element of $x : \tya \vee \tyb$. If the tag is true,
+then we know that the second element is of type $\tya$, and we will apply $f$.
+The same applies to the other branch, with $\tyb$ and $g$.
+
+\subsubsection{Naturals and similarly lists}
+
+Now it's time to showcase the power of $\mathsf{W}$ types.
+
+\begin{eqnarray*}
+ \mathsf{Nat} & = & \lcw{b}{\lcbool}{\abs{b}{\lcite{b}{\top}{\bot}}} \\
+ \mathsf{zero} & = & \lcfalse \lhd \abs{z}{\lcabsurd z} \\
+ \mathsf{suc} & = & \abs{n}{(\lctrue \lhd \abs{\_}{n})} \\
+ \mathsf{plus} & = & \abs{x\appspace y}{\lcrecz{x}{\abs{b}{\lcite{b}{\abs{\_\appspace f}{\app{\mathsf{suc}}{(\app{f}{\lcunit})}}}{\abs{\_\appspace\_}{y}}}}}
+\end{eqnarray*}