Say something about existentials versus sum types.

1 files changed, 42 insertions, 0 deletions

diff --git a/transp-inf110-03-super.tex b/transp-inf110-03-super.tex
index 1201c29..79b9570 100644
--- a/transp-inf110-03-super.tex
+++ b/transp-inf110-03-super.tex
@@ -226,6 +226,48 @@ $x_0$ correspondant dans autre chose qu'une preuve.  {\footnotesize
 \end{frame}
 %
 \begin{frame}
+\frametitle{Le problème du $\exists$ et des types sommes}
+
+Doit-on croire à ceci (pour $U$ et $V$ deux types) ?
+\[
+(\forall(x:U).\,\exists(y:V).\,P(x,y))
+\Rightarrow
+(\exists(f:U\Rightarrow V).\,\forall(x:U).\,P(x,f(x)))
+\]
+
+\medskip
+
+{\footnotesize (Cet énoncé porte le nom d'\alert{axiome du choix} :
+  c'est un analogue pour la théorie des types de l'axiome du choix (de
+  Zermelo) en théorie des ensembles.)\par}
+
+\medskip
+
+\itempoint Si on voit $\forall$ et $\exists$ comme des types produit
+et \alert{somme} en famille respectivement, \alert{oui} :
+$\forall(x:U).\,\exists(y:V).\,P(x,y)$ représente une fonction qui
+prend un $x$ de type $U$ et renvoie un $y$ de type $V$ ainsi qu'un
+$P(x,y)$ correspondant : on peut collecter tous ces $y$ en une
+fonction $f : U \Rightarrow V$.
+
+\medskip
+
+\itempoint Si on voit $\exists$ comme un quantificateur
+\alert{logique}, alors \alert{non} : le $y$ renvoyé par $\exists$ ne
+peut servir qu'à l'intérieur d'une preuve, pas être collecté en une
+fonction.
+
+\medskip
+
+\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).
+
+\end{frame}
+%
+\begin{frame}
 \frametitle{Imprédicativité}
 
 \itempoint On appelle \textbf{imprédicativité} la possibilité de