Slightly rework slide on \exists versus sum types.

1 files changed, 19 insertions, 1 deletions

diff --git a/transp-inf110-03-quantif.tex b/transp-inf110-03-quantif.tex
index 867d04d..0e1891f 100644
--- a/transp-inf110-03-quantif.tex
+++ b/transp-inf110-03-quantif.tex
@@ -528,6 +528,20 @@ Doit-on croire à ceci (pour $U$ et $V$ deux types) ?
 \Rightarrow
 (\exists(f:U\Rightarrow V).\,\forall(x:U).\,P(x,f(x)))
 \]
+{\footnotesize
+\[
+\begin{aligned}
+\text{« preuve(?) » :~}
+\lambda(h:\cdots).\,
+\langle
+&\lambda(x:U).\,
+(\texttt{match~}hx\texttt{~with~}\langle v,z\rangle \mapsto v),\\
+&\lambda(x:U).\,
+(\texttt{match~}hx\texttt{~with~}\langle v,z\rangle \mapsto z)
+\rangle
+\end{aligned}
+\]
+\par}
 
 \medskip
 
@@ -553,11 +567,15 @@ fonction.
 
 \medskip
 
+{\footnotesize
+
 \itempoint C'est ici la différence principale entre des systèmes comme
 Coq (où l'énoncé ci-dessus ne sera pas prouvable pour $P : U\times V
 \to \mathit{Prop}$) et les systèmes à la Martin-Löf comme Agda (où
 Curry-Howard est suivi « jusqu'au bout » : il n'y a pas de $\exists$
-uniquement logique, et cet énoncé est prouvable).
+uniquement logique, et cet énoncé est prouvable comme indiqué).
+
+\par}
 
 \end{frame}
 %