From be85cf0706034f445fc29f0872785727db123a40 Mon Sep 17 00:00:00 2001
From: "David A. Madore" <david+git@madore.org>
Date: Tue, 19 Dec 2023 10:34:09 +0100
Subject: Say something about existentials versus sum types.

---
 transp-inf110-03-super.tex | 42 ++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 42 insertions(+)

(limited to 'transp-inf110-03-super.tex')

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
@@ -223,6 +223,48 @@ $x_0$ correspondant dans autre chose qu'une preuve.  {\footnotesize
   (Les détails dépendent du système logique précis considéré {\tiny et
     si Martin-Löf est dans la salle}.)}
 
+\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}
-- 
cgit v1.2.3