Saut fondationnel
Afin de ne pas polluer un autre fil, où
j'ai donné mon avis sur le "fameux (c'est lui?) livre qui introduit à la théorie homotopique des types
j'ouvre un fil indépendant pour rappeler (car il me semble que je l'ai déjà fait) en quoi consisterait forcément un progrès de NATURE dans les fondations de la science (ie des maths). Je chercherai le fil où j'en ai déjà parlé et mettrai un lien, mais je pense que je peux en peu de temps taper les idées essentielles.
1/ Actuellement on a un "gros problème" (j'appelle ça problème pour l'occasion, mais ça ne signifie rien): le seul signe que nous ne définissons pas (ou un des seuls**) n'est pas associatif.
2/ On peut retrouver de l'associativité, mais au prix de tricheries, dont le sentiment est de toute façon qu'elles n'apportent pas grand chose.
3/ Précisions:
3.1/ ce signe est l'espace entre les mots (en théorie des ensembles, il est noté $\in$ par assumation, ailleurs, il est noté avec le code ascii numéro 32, donc moins assumé, mais les pros savent "le voir" (enfin dans 75% des cas disons, ils dérapent un peu, mais se rattrapent dans 25% des cas)
3.2/ Afin d'éviter les symboles de fonctions (qui obligent à construire des termes, les logiciens savent à quel point c'est chaint les termes) et privilégier plutôt une unique relation binaire, les hommes (et les femmes ? :-D ) semblent avoir décidé qu'on doit obtenir un truc dont le statut est d'être une phrase dès lors qu'il est mis entre deux mots, mais ce n'est pas du tout important. L'important, et c'est comme ça qu'il faut le voir, c'est qu'il n'est pas associatif et qu'il désigne (enfin qu'il est appelé en toute généralité) "l'application" (même si en TDE, il est appelé "appartenance"). Du coup au lieu de "fonction", les mots ont reçu un statut qui s'appelle "ensemble", etc.
4/ "pas associatif" : bin tout simplement on n'a pas $(a\in b)\in c = a\in (b\in c)$ (et dans le cas général, on n'a pas $(f(g))(h) = f(g(h))$)
5/ Une tricherie élégante et connue consiste à rajouter un seul symbole (je l'appelle $K$, c'est assez traditionnel) à supposer que $\forall x: (Kx)y = x$ et à remarquer qu'alors $[f(g) = h] \iff f\circ [ (K(g)) = K(h)]$. Hélas, on sent que c'est "tricher", même si les catégoriciens ont fait un usage pertinent de ce truc.
6/ Tout présenter sous forme catégorielle (une catégorie est un couple $(E,*)$ où $*$ est une fonction partielle associative allant de $E^2$ dans $E$ ) a présenté de nombreux avantages pour bien des professionnels de l'algèbre, mais ils travaillent sur des théories qui semblent tout en bas de la hiérarchie définie par la consistency-strength et on peut facilement prouver que ce sont les seules qui sont "typables". Par ailleurs, pour arriver à reparler de "Ap" (ie de $\in$) tout en faisant mine de ne pas en parler, on doit passer par une véritable offensive militaire nucléaire (inventer les catégories cartésiennes fermées, et même les topos, ou les catégories monoidales, etc)
7/ Bref, en conclusion, la plus grande thèse du 21 ième siècle sera écrite par le jeunot qui saura rendre les maths associatives (sans tricher). Ce n'est pas un énoncé formel, mais j'espère quand-même que je me suis fait comprendre par les lecteurs motivés.
8/ Actuellement, mais ce n'est pas très folichon, même les machines de Turing (pourtant de la famille des problèmes de monoides associatifs (ou magma je ne sais plus comment on dit)) sont "incorrectement" localisées***, puisqu'il faut deux grammaires algébriques et un renversement. On a besoin (évidemment) de parenthèses (ou de l'écriture polonaise) en LC, bref, l'associativité au sommet (ou à la racine) de l'arbre fondationnel ne semble pas facile à trouver si elle existe.
*** une suite de mots $u_1,u_2,...,u_n$ de mots telle que deux mots qui se suivent dans la suite sont un "pas" de la MT T ne peut pas être présentée telle quelle si on ne dispose que de langages algébriques. Une GL ne peut reconnaitre que les mots de la forme $u|renverse(v)$ tels que (u,v) correspond à un pas d'exécution. Ainsi un "calcul turingien" doit être offert à une MT sous la forme suivante: $u_1,v_2,u_3,v_4,...$ et il faut demander si $u_1v_2-u_3v_4-...$ est dans $G_1$ ET si $v_2u_3-v_4u_5-...$ est dans $G_2$ (les $G_i$ étant des langages algébriques) pour savoir si $u_1,u_2,...$ est un exécution correcte de programme, avec $v_i := renverse(u_i)$.
** même $\forall $ est définissable in some sense par $[\forall xR(x)] := [(x\mapsto R(x))=constante(vrai)]$. Mais dans ce cas, il ne faut pas définir $(x=y)$ par $\forall a: (a(x)\to a(y))$ :-D
j'ai donné mon avis sur le "fameux (c'est lui?) livre qui introduit à la théorie homotopique des types
j'ouvre un fil indépendant pour rappeler (car il me semble que je l'ai déjà fait) en quoi consisterait forcément un progrès de NATURE dans les fondations de la science (ie des maths). Je chercherai le fil où j'en ai déjà parlé et mettrai un lien, mais je pense que je peux en peu de temps taper les idées essentielles.
1/ Actuellement on a un "gros problème" (j'appelle ça problème pour l'occasion, mais ça ne signifie rien): le seul signe que nous ne définissons pas (ou un des seuls**) n'est pas associatif.
2/ On peut retrouver de l'associativité, mais au prix de tricheries, dont le sentiment est de toute façon qu'elles n'apportent pas grand chose.
3/ Précisions:
3.1/ ce signe est l'espace entre les mots (en théorie des ensembles, il est noté $\in$ par assumation, ailleurs, il est noté avec le code ascii numéro 32, donc moins assumé, mais les pros savent "le voir" (enfin dans 75% des cas disons, ils dérapent un peu, mais se rattrapent dans 25% des cas)
3.2/ Afin d'éviter les symboles de fonctions (qui obligent à construire des termes, les logiciens savent à quel point c'est chaint les termes) et privilégier plutôt une unique relation binaire, les hommes (et les femmes ? :-D ) semblent avoir décidé qu'on doit obtenir un truc dont le statut est d'être une phrase dès lors qu'il est mis entre deux mots, mais ce n'est pas du tout important. L'important, et c'est comme ça qu'il faut le voir, c'est qu'il n'est pas associatif et qu'il désigne (enfin qu'il est appelé en toute généralité) "l'application" (même si en TDE, il est appelé "appartenance"). Du coup au lieu de "fonction", les mots ont reçu un statut qui s'appelle "ensemble", etc.
4/ "pas associatif" : bin tout simplement on n'a pas $(a\in b)\in c = a\in (b\in c)$ (et dans le cas général, on n'a pas $(f(g))(h) = f(g(h))$)
5/ Une tricherie élégante et connue consiste à rajouter un seul symbole (je l'appelle $K$, c'est assez traditionnel) à supposer que $\forall x: (Kx)y = x$ et à remarquer qu'alors $[f(g) = h] \iff f\circ [ (K(g)) = K(h)]$. Hélas, on sent que c'est "tricher", même si les catégoriciens ont fait un usage pertinent de ce truc.
6/ Tout présenter sous forme catégorielle (une catégorie est un couple $(E,*)$ où $*$ est une fonction partielle associative allant de $E^2$ dans $E$ ) a présenté de nombreux avantages pour bien des professionnels de l'algèbre, mais ils travaillent sur des théories qui semblent tout en bas de la hiérarchie définie par la consistency-strength et on peut facilement prouver que ce sont les seules qui sont "typables". Par ailleurs, pour arriver à reparler de "Ap" (ie de $\in$) tout en faisant mine de ne pas en parler, on doit passer par une véritable offensive militaire nucléaire (inventer les catégories cartésiennes fermées, et même les topos, ou les catégories monoidales, etc)
7/ Bref, en conclusion, la plus grande thèse du 21 ième siècle sera écrite par le jeunot qui saura rendre les maths associatives (sans tricher). Ce n'est pas un énoncé formel, mais j'espère quand-même que je me suis fait comprendre par les lecteurs motivés.
8/ Actuellement, mais ce n'est pas très folichon, même les machines de Turing (pourtant de la famille des problèmes de monoides associatifs (ou magma je ne sais plus comment on dit)) sont "incorrectement" localisées***, puisqu'il faut deux grammaires algébriques et un renversement. On a besoin (évidemment) de parenthèses (ou de l'écriture polonaise) en LC, bref, l'associativité au sommet (ou à la racine) de l'arbre fondationnel ne semble pas facile à trouver si elle existe.
*** une suite de mots $u_1,u_2,...,u_n$ de mots telle que deux mots qui se suivent dans la suite sont un "pas" de la MT T ne peut pas être présentée telle quelle si on ne dispose que de langages algébriques. Une GL ne peut reconnaitre que les mots de la forme $u|renverse(v)$ tels que (u,v) correspond à un pas d'exécution. Ainsi un "calcul turingien" doit être offert à une MT sous la forme suivante: $u_1,v_2,u_3,v_4,...$ et il faut demander si $u_1v_2-u_3v_4-...$ est dans $G_1$ ET si $v_2u_3-v_4u_5-...$ est dans $G_2$ (les $G_i$ étant des langages algébriques) pour savoir si $u_1,u_2,...$ est un exécution correcte de programme, avec $v_i := renverse(u_i)$.
** même $\forall $ est définissable in some sense par $[\forall xR(x)] := [(x\mapsto R(x))=constante(vrai)]$. Mais dans ce cas, il ne faut pas définir $(x=y)$ par $\forall a: (a(x)\to a(y))$ :-D
Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
Connectez-vous ou Inscrivez-vous pour répondre.
Réponses
Regadez bien $A\to A$. Peut-être avez-vous l'impression de lire "A implique A". Ou peut-être avez-vous l'impression de lire "ensemble des applications de $A$ dans $A$. Dans tous les cas, vous avez une spécificité c'est que $A\to A$ est un théorème si vous le lisez comme une phrase avec $\to$ qui signifie "implique" et que $A\to A$ n'est pas vide si vous le lisez comme un ensemble.
Qu'il ne soit pas vide n'est certes pas un grand événément puisqu'il n'y a .... qu'un seul ensemble vide :-D Donc les ensembles vides sont rares.
Mais ce qui fait la spécifité de la suite de caractère $<< A ; \to; A>>$, c'est que même sans connaitre $A$, vous pouvez désigner un élément bien précis de $A\to A$. Autrement dit, pas besoin de l'axiome du choix pour construire une fonction $\phi$ définie sur $E$ (qui que soit $E$), telle que $\forall A\in E: (\phi (A\to A) \in (A\to A))$.
Et bien ce phénomène est général s'appelle "la correspondance de Curry Howard" et quand on invente des signes en tout genre pour nommer ces fonctions choix canoniques comme l'est $\phi$, on abrège (ou on mémorise) des choses qui s'exécutent informatiquement et les mêmes choses (sans changer un seul caractère!!!) sont lisibles comme étant des preuves de maths. A noter que quand on efface "les types", on obtient le même programme, mais on n'est plus "renseigné" sur le fait qu'il est "sécurisé" (les programmes typés terminent, pour le dire en caricaturant)
Par exemple, $\phi$ qui à chaque couple $(A,B)$ pick the element $(x,y)\to x$ of $[(A\times \to A]$ est un programme qui jette une des ressources qui lui est présentée dans $(x,y)$ en ne gardant que $x$.
Le traité du fil en lien étudie sur plusieurs centaines de pages une chose très simple, qui se résume en:
Etant une fonction $f$ très simple de domaine $E$ inconnu, quand est-ce qu'on peut trouver une fonction $g$ (simple ou pas, mais sans l'axiome du choix) telle que $\forall x\in E: g(x)\in f(x)$.
(Ca s'appelle un résumé en 2 lignes et on peut réécrire le traité seul si on a compris ça :-D (outrance outrance dire que j'ai appris ce mot récemment))
La lecture en diagonale me semble me montrer que le livre ne fait pas grand chose d'autre, même s'il appelle ça autrement. Pourquoi ses auteurs ont-ils besoin de typer?
Bin la réponse est très simple: si on veut gérer les quantificateurs dans cet amusant paradigme et qu'on ne s'est pas spécialisé en TDE, on croit qu'on est dans la m...e: en effet, la PHRASE suivante:
$$\forall x: R(x)\to S(x)$$
joue le rôle de poil à gratter pour ces auteurs car ils devraient la traduire par :
$$ \prod_{x\in ToutLuniverToutentier} (S(x)^{R(x)})$$
Gros objet, n'est-ce pas? Mais c'est pas fini, car ce qui les intéresse, c'est de faire varier le couple $R,S$ :-D !! Ils n'ont donc pas envie de cherche
$\phi$ qui à chaque $R,S$ (allant moralement de l'univers dans ValVerites) associe une fonction $\phi(R,S)$ qui ... à chaque élément de l'univers $x$ associe un élément de $S(x)^{R(x)}$.
Donc, pour des raisons de "terreur psychologiques", ils préfèrent
$$ \prod_{x\in UnZentilPetitEnsemble} (S(x)^{R(x)})$$
etc, etc. Ce qui donne à la fin:
$$\forall x\in LeZentilPetitEnsemble: R(x)\to S(x)$$
Bon, j'espère que quand je reparcourerai le livre, je trouverai des "vrais trucs" en provenance de la recherche en topologie algébrique et pas juste le fait qu'on y consomme de grandes cuillères de "fonctions canoniques" allant d'espaces pointés dans d'autres. Si c'est juste pour ça que le mot "homotopique" a fait son entrée, c'est un peu tristounet.
J'espère avoir été dans de la bonne outrance :-D Evidemment, j'espère me tromper
Déjà je t'ai vu à plusieurs reprises expliquer que la topologie algébrique était actuellement encore une mauvaise théorie, immature et qu'on n'y comprenait rien. Il faudra expliquer ce que tu entends par là et pourquoi tu penses qu'une avancée en théorie des ensembles impliquerait une avancée en topologie algébrique.
Ensuite, concernant le livre dont tu parles, certes il s'amuse à aller sur des terrains sur lesquels il ne devrait pas entrer mais je peux assurer que la nécessité des "hautes théories homotopiques" pour résoudre des problèmes de géométrie en haute dimension n'est plus à prouver. Accessoirement, je vois qu'il y a Voïevodski dans les auteurs, ce qui me laisse à penser que c'est vraiment pas un livre rempli de couillonnades. :-D
Enfin, je trouve ton parallélisme entre $\in$ et l'espace entre les mots très discutable. Bon déjà et tu l'expliques toi-même la comparaison ne tient pas car le $\in$ n'est pas associatif alors que l'espace entre les mots l'est évidemment. C'est clair que pour tout le monde (je suis) matheux est équivalent à je (suis matheux) et donc on peut enlever les parenthèses. Maintenant si le but c'est d'avoir en théorie des ensembles, un symbole qui représente VRAIMENT l'espace entre les mots bah je ne vois pas ce qui gêne. Il suffit de repartir de zéro, choisir son symbole favori dans l'alphabet à disposition et d'en définir les axiomes. Par exemple on peut mettre l'associativité en axiome ainsi que l'idempotence. (Parce qu'en général mettre deux espaces entre deux mots c'est pareil, sémantiquement, qu'en mettre un seul. Alors que $\in \in$ est quelque chose qui pose problème en général. :-D )
"mauvaise", je ne sais pas si j'ai dit ça, mais je pense qu'effectivement, elle n'est pas encore assez "logique", en ce sens qu'on a l'impression que ses spécialistes la "découvre" comme les physiciens font leur découverte.
Par contre, je pense qu'il y a des gens qui en ont une vision de spécialiste unifiée par la force de l'habitude et la trouvent donc compréhensible.
Ce n'est pas ça que j'ai dit, ni que je pense. Ce que je pense est qu'elle sert de critère, à savoir qu'on "aura compris quelque chose" le jour où elle deviendra "triviale", car on aura trouvé et prouvé "le bon énoncé". Un peu comme la topologie générale a été trivialisée par l'ANS (400 pages de topologie générale sont devenues inutiles à lire puisque 3 axiomes d'une ligne et quelques petits exercices de familiarisation suffisent à rendre triviales ces 400 pages).
Je veux bien te croire et te faire confiance, tu as l'air de savoir de quoi tu parles et la motivation qui t'anime. Cependant, je pense que ce n'est pas ce traité (que j'ai l'impression peut-être à tort, que je pourrais écrire en quelques heures en sifflotant) qui parle d'homotopie, comme je l'ai dit. Faire connaitre au grand public que les preuves et les fonctions canoniques c'est la même chose est surement une bonne action, mais c'est beaucoup moins unifiant que ce que l'on peut imaginer. J'ai peur que ce ne soit là qu'une entreprise de plus de publicité. D'ailleurs, la preuve: je connais tout ça sans avoir le moins du monde progressé en Top.Alg. Et quand je dis "je connais", c'est carrément au niveau des tripes, je veux dire que "ça m'habite" en profondeur, il ne s'agit pas de "connaissances".
Maintenant, comme je l'ai dit, je n'ai fait que parcourir le livre pendant une trentaine de minutes (et même si c'est 1H et ai mal évalué), j'ai peut-être raté les bons passages à grosse plus value. Pour te dire, j'ai même l'impression d'avoir plus trouvé de fond quand j'ai fait l'effort d'acquérir les topos, mais peut-être était-ce parce que je les abordais du mauvais bout et ai subi un syndrome de Stockholm en faisant tomber quelques incompréhensions, j'avoue.
oupssss, tu m'as mal lu ou je me suis mal exprimé. Je n'ai pas parlé de parallèle, j'ai dit que $\in $ EST l'espace entre les mots. . En particulier, j'ai dit que ni cet espace, ni $\in$ (qui sont le même objet) ne sont associatif.
Absolument pas!!! Je pense que tu confonds la présence tacite de parenthèses en priorité à gauche avec l'associativité. On écrit juste A B C au lieu de (A C pour économiser de l'encre. Par ailleurs, je me répète $a\in b$ n'est rien d'autre que $b(a)$. La tradition scientifique d'assumer les choses a juste, ici, joué en faveur de l'utilisation d'un signe, plutôt que garder l'espace.
Je n'ai pas besoin de répondre à la fin de ton post du coup.
Je souhaiterais être bien compris. Les maths (et la science) sont basées sur la notion d'abréviations paramétrées, ce qui a conduit l'humanité à conventionner l'enregistrement des énoncés en faisant semblant de croire qu'ils sont formulés dans le cadre ZF(C) alors qu'ils sont formulés dans le cadre bien plus simple, mais toujours ensembliste de la TDE générale (celle qui est contradictoire), où il n'y a pas d'axiomes en dehors de l'extensionnalité, mais où "des axiomes automatiques réalisés (au sens de la réalisabilité) par l'identité (l'action qui ne fait rien) sont générés tout seuls par la langage, en abrégeant: tu connais le célébrissime $<<$ en abrégeant par $a(x) := non(x(x))$, on obtient $a(a)=non(a(a))>>$.
En termes déductifs, ce n'est rien d'autre que l'application de l'axiome $(\forall xR(x)) \to Q$ où $Q$ est obtenu en remplaçant toutes les occurrences des $z\in x$ où $x$ est libre dans $R$ par $S(z)$, que les gens appliquent même assez souvent sans s'en apercevoir. Sans la crise des fondements, aujourd'hui, la plupart des scientifiques considèreraient même qu'il ne se passe rien, que c'est comme $A\to A$. Comme ça a été célèbrement contradictoire, on fait attention. Mais ça ne change rien. C'est juste une affaire de pointeur, la crise des fondements n'ayant en aucun cas rendu impossible de faire pointer le sigle $a(x)$ sur $f(x(x))$. Je ne crois pas qu'il soit sain de "faire semblant" de boycotter certaines boucles et pas d'autres, car rien ne légitime celles qui reste, si ce n'est que expérimentalement, on n'a pas encore eu de contradiction.
Je veux bien te croire que cela puisse marcher pour la topologie générale mais même là je suppose que tu parles de la topologie générale "de base". (Celle où les théorèmes les plus compliqués sont Urysohn et Tychonoff) En topologie algébrique en tout cas, l'homologie singulière est une théorie très bien digérée et très accessible aujourd'hui. Le problème c'est que cet outil est moins puissant que la théorie homotopique et, celle-là en revanche, est moins facilement digérable.
J'avais en effet mal compris ton histoire d'espace entre les mots. Je pensais que tu voulais dire que le formalisme ensembliste à base de $\in$ n'était que la formalisation naturelle de notre manière de nous exprimer dans notre langue maternelle. Mais cela dit, en y pensant, quand on lit une phrase en français, on la lit de gauche à droite donc peut-être qu'en effet on parenthèse automatiquement à gauche. Par contre je maintiens, en tout cas en français, que la phrase ne change pas de sens en rajoutant des espaces et que donc on devrait pouvoir dire des trucs du style $a \in \in b = a \in b.$
PS : Les romains de l'antiquité écrivaient leur langue sans aucun espace (scripta continua). Peut-être est-ce lié à la pauvreté mathématique de ce peuple. :-D
C'est le coup du Fixed point combinator ?
--
PS : Heureusement, Christophe, que tu précises : parce que du paragraphe qui suit, je ne comprends pas un traître mot ! B-)
cc a du mal à se relever de la contradiction naïve des ensembles, qui est la soeur, l'épouse de Zeus : Hera.
Il t'expliquera tout ça : de la création à l'incréation.
Salut fondationnel ceci dit.
S
@marsup: c'est très simple. On utilise des tas de boucles, mais on a dû se forcer, semble-t-il (je n'y étais pas) face à la définition $a(x):=ChapeauDe(x(x))$ (appliquée, comme toute définition, $\forall x$) au motif que ça donne un point fixe à la fonction $ChapeauDe$ à faire semblant de croire que cette fonction n'existe pas (alors que tu l'as sous les yeux).
De là, une itinérance qui a été extrêmement pénalisante pour la recherche, même si physique et maths travaillent à bas niveau pour la construction des machines industrielles.
Pour te le dire autrement, on a eu une sorte de "peur religieuse" devant $E:=\{x\mid x\in x\to P\}$ au motif qu'un simple raisonnement intuitionniste permet d'en déduire $P$.
Ca a été à mon avis une erreur (et je pourrais être celui dont on attend la réaction opposée en tant que logicien qui voudrait préserver l'absoluité de la logique propositionnelle), de renoncer à une démarche complètement claire d'abréviation (bin voui, ça boucle et alors) juste pour "garder" la logique classique ou intuitionniste (les 2 sont très proches et tout autant incompatibles avec le fait que $vrai\neq faux$ dès lors qu'elles exploitent $E$.
Je souhaite que cette erreur de parcours se résorbent (certes ça se fera doucement). Il est triste qu'il ait fallu attendre la théorie quantique (mais surtout sa construction imposée de force par la Nature à l'homme et dans la douleur) pour accepter de parler avec des phrases égales à leur négation. (La TQ nous offre A:=[vrai+faux], qui vérifie non(A)=A, car non(A) = [faux+vrai] et le + de la TQ est commutatif (et toutes les fonctions logiques sont additives).
Ce n'est pas en continuant aveuglément sur cette lancée de recherche ad hoc de consistance au doigt mouillé (avec le livre dont on débat, mais aussi les catégories, etc) qu'on va réparer cette faute de parcours (ou cette crainte religieuse de l'univers "trop gros" pour ne pas rendre faux égale à vrai quand on peut cloner*** des ressources).
@Cyrano: concernant mon premier post, la présence de deux opérations si tu préfères l'une associative et l'autre non, vérifiant $\forall x,y,z: (x\circ y)*z = x*(y*z)$ est LE problème que je décris, voulant dire que le jeunot qui nous ramènera ça à une seule, qui de plus sera associative fera faire un bond à la science. Le paradigme catégorique "essaie" très timidement de prendre ce défi en charge, mais s'est noyé depuis longtemps dans des ajouts d'axiomes en tout genre, comme tu le sais mieux que moi (la liste des adjectifs, parmi lesquels, cartésiennes fermées, monoidales, etc, figurent est très longue), pour compenser sa "seule opération $\circ$". Bon de toute façon les cat cherchent aussi d'autres contrées que celle de l'amont des maths.
*** à marsup, il n'y a rien de "spécialement puissant" dans une phrase $a$ telle que $a=(a\to b)$, à part que la cloner te donne $b$ avec la procédure:
De $a$, je passe à $a$ ETADD $a$, autrement dit $a$ ETADD $(a\to b)$, qui me donne $b$. Cela prouve que je peux échanger contre deux ressources $a$ que je donne la ressource $b$, autrement dit j'ai $a\to (a\to b)$ qui est un théorème. Si j'admets que je dispose de $[a\to (a\to b)]\to (a\to b)$, ça me permet d'acquérir $a\to b$, qui lui-même est $a$. Je le clone et je l'échange contre $b$, ce qui me prouve $b$.
Sauf que les seules choses qu'on peut cloner ce sont les "vérités immuables" d'une certaine nature puisqu'une photocopie de leur preuve suffit. Pour les autres, c'est complètement idiot de prétendre qu'on peut les dupliquer à volonté. Chaque jour nous fait subir notre incapacité de dupliquer nos billets de 20 euros :-D (même s'ils ne sont pas des phrases, on voit bien que dupliquer n'est pas une chose gratuite. Précisément: que dupliquer, même des garanties de phrases ne devrait pas être évalué à prix nul).
Alors là je suis bien d'accord. Personnellement je n'utilise les catégories que pour résoudre des vrais problèmes d'analyse, pas pour réinventer la sauce.
J'ai davantage regardé le livre et effectivement je suis déçu. Cela ne parle pas vraiment des hautes théories homotopiques (celles qui permettent réellement de résoudre des problèmes de géométrie en haute dimension), c'est plutôt un gros baratin pour montrer un joli formalisme qui permet de retrouver des concepts très classiques. C'est le genre de truc très joli à voir mais comme d'habitude le coup "notre formalisme permettra de mieux comprendre des choses qu'on ne comprenait pas en théorie des ensembles" me semble d'une grande naïveté.