From e5dbc019a4f4083087cf3a81ab7a1024a08fbf90 Mon Sep 17 00:00:00 2001
From: "David A. Madore" <david+git@madore.org>
Date: Sun, 7 Jan 2024 19:11:26 +0100
Subject: Slightly rework slide on \exists versus sum types.

---
 transp-inf110-03-quantif.tex | 20 +++++++++++++++++++-
 1 file changed, 19 insertions(+), 1 deletion(-)

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}
 %
-- 
cgit v1.2.3