Additional material for section 2

itp-lesson/main.tex

@@ -715,6 +715,16 @@ ghci> \textcolor{emph2}{let} p \textcolor{emph2}{::} P\textcolor{emph2}{;} p = \
 	\end{center}
 \end{frame}
 
+%% If too short:
+%% - BHK interpretation for "or", "exists", "false", "negation"
+%% - what reduction corresponds to (e.g. fst (a, b) is cut elimination)
+%% - exercise:
+%%   - encode pairs using arrows
+%%   - considering the BHK interpretaton of the existential,
+%%     encode the existential quantification in the universal
+%%     quantification
+
+
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %% REMOVED in favour of BHK interpretation
 %