Catégories et types

cela dit c'est de bonne guerre comme je disais d'utiliser un outil matériel pour m'empêcher de participer à une discussion point cela me fait penser qu'il faudra que je re négocié avec la modération, maintenant que je suis déjà dictionnaire du forum, une ouverture de tous mes droits ce qui m'inspire cette remarque c'est de voir que l'autre fils ne va pas t'apporter grand-chose apparemment si j'en juge par le début entre parenthèses humour.

Bon je laisse ce post rigolo sous la dictée je promet de le réparer pl us tard la j'ai une urgence. Exercice: deviner ce que j'ai dicté en lisant ce que le télé a écrit.

@ignatus. J'ai oublié de te répondre sur Voedovski. Bin c'est évident qu'il y a un loup si besoin d'un savant ou d'une autorité. Que ces travaux produisent un bon algo pour calculer les groupes d'homotopie et que ça mérite un MF je suis plus que d'accord que tant mieux. Mais ça n'a.vraiment strictement rien à voir avec des fondements. C'est même un critère quasiment absolu: aucune chance d'avoir des fondements si besoin de caution. Je ne parle pas que pour ça mais pour toute forme d'ambition similaire avenir éventuelle.

@ignatus : je change d'avis je te remercie d'avoir ouvert un fil parent en algèbre au fond. En principe tu devrais classiquement assister à tout un tas de décompensations marrantes où pour faire semblant de ne pas utiliser les mots ensembles (ie fonctions =ensembles) etc tu vas voir déferler des "from x je me donne f(x), g(x)"; "je me donne hom(À,B) une collection dite de flèches;" etc.

http://www.les-mathematiques.net/phorum/read.php?3,1880072,1880306#msg-1880306 (ce n'est qu'un exemple)

Je m'en veux effectivement si j'ai pu intimider ces exhibitions de ridicule involontaires car à mon corps défendant j'aurais joué le rôle de tabou ce qui n'est pas mon intention. En effet, il me semble préférable de laisser ces ridiculisations se produire pour mieux les dénoncer ensuite. J'ai eu le tort de réagir comme si tout le monde se souvenait de les avoir déjà vues et de commencer les coms postérieurs.

Je me permets de signaler que l'opinion que "tout est TDE" (en particulier théorie des types est TDE, donc dire "en types, pas tde" serait une faute) n'est pas du tout partagée par tout le monde : il s'agit bien d'une opinion.

Bien sûr qu'on suppose. Mais supposer ne veut pas dire magiquement "théorie des ensembles" :-D Même si je sais bien que c'est ce que tu défends.
(J'imagine que tu vois que le problème de ta phrase est que si n'importe qui n'est pas d'accord, tu pourras simplement dire "ah, cette personne est militante" et donc automatiquement discarder son argument. "toute personne non militante est d'accord avec moi, ou n'y a pas réfléchi" empêche automatiquement tout dialogue)

christophe c a écrit:

"from x je me donne f(x), g(x)"; "je me donne hom(À,B)

Tu prends vraiment les gens pour des imbéciles...
Tu sais bien qu'aux variations près ils veulent dire "pour nous une fonction/une flèche de $A$ dans $B$ va être un objet de type $A\to B$" (on est en lambda calcul typé). Ce ne sont pas des inspecteurs. Si défaut de communication il y a, c'est sur la manipulation des lettres liées ... que les gens qui gravitent autour du lambda calcul connaissent déjà.

À bin non il est perdu (j'ai éteint et rallumé)

Foys: relis ce que j'ai écrit je crois que tu fais un contre sens. Tu dis comme moi en semblant me contredire.

La réponse que j'ai faite à Max est perdue je la recevrai.

Une fois de plus je rappelle que seul l'operatoire compte. Appeler "collection ou type" les ensembles ne change rien OPERATOIREMENT.

De même qu'ecrire u dans {x/..} ou écrire (x mapto ..) (u) ne change STRICTEMENT RIEN.

Personne n'a jamais eu l'idée de prétendre que TDE et lambda calcul sont différents, parce que c'est un monde de logiciens honnêtes qui ne font pas semblant. De même personne de sérieux et expérimentée n'ira me contredire car sait que la chimère du transcendance magique est "trop espéré" chez les débutants abusés (qui par exemple croient que HoTT ou les catégories ne dont pas après et faits dans la TDE).

Hélas avec ma maladresse et les ambiguïtés je suis le seul à jouer la sale rôle. Bon bin tant pis. Ce sont t des.gens comme ignatus et autres étudiants à qui on a fait des annonces superlative qui paient pas moi.

Christophe : Je n'ai pas nourri la chimère, j'ai simplement fait remarquer que c'était une opinion (ce qui est le cas) :-D
Déjà si tu fais tout syntaxiquement, la question n'a pas de sens; et ensuite les égalités "dures" que tu suggères, tu ne les as jamais justifiées, de même que la plupart de ce que tu affirmes sur les fondements. Je l'ai déjà dit plus tôt, je serais ravi d'en apprendre plus sur ta vision des fondements si tu écrivais un truc dessus à un moment, un truc propre - et pas simplement comme ce que tu as fait sur ce fil, une suite d'affirmations "non idéologiques puisque c'est toi qui les dis" ;-)

Je le répète (et là c'est un point méta discours, complètement indépendant du sujet ) : dire que par défaut toutes les personnes qui ne sont pas d'accord avec toi n'ont pas assez réfléchi, ou ne sont pas honnêtes (celui-là tu le dis moins, enfin tu le dis par contraposée seulement), ou encore sont militantes (et donc rejeter leur point de vue automatiquement) ne permet pas de dialoguer; puisque l'autre côté est délégitimé sans mot dire. Tu devrais donc peut-être te débarrasser de cette habitude (:P) (indépendamment du sujet à nouveau !)

Plus sur le sujet spécifiquement : il ne faut pas oublier que tu utilises les mêmes mots que nous mais pas toujours avec le même sens, par exemple tu donnes aux mots "théorie des ensembles" un autre sens que celui qui est communément accepté - et comme tu n'as jamais précisé ce que tu entendais vraiment par là (enfin tu l'as peut-être fait il y a des années, mais on n'étais pas tou.te.s là à ce moment :-D ), ça fait encore plus dialogue de sourd : d'un côté tu n'écoutes pas les autres parce qu'iels sont militant.e.s, et de l'autre iels ne peuvent pas t'écouter puisque tu utilises des mots avec un sens différent et ne détaille jamais ta position.

Comme je l'ai dit dans le post parallèle d'ignatus, je m'en veux un peu d'avoir fait dévier son fil... ignatus a réagi avec un post parallèle, dont j'espère qu'il ne sera pas perturbé de la même manière, donc je m'en veux un peu moins de continuer la déviation sur celui-là mais tout de même.

Foys: attention, tu es à la limite du militantisme là (:P)

C'était loin d'être évident pour moi, désolé. Je ne suis pas aussi doué que tu le crois :-D
Par contre je veux bien que tu précises alors ce que tu entends par "modèle dans ZFC" : si tu parles de modéliser la syntaxe, je n'ai aucun souci, mais ça n'a que peu d'intérêt.
Maintenant, si tu parles de sémantique, il faut préciser un peu plus. Je prends l'exemple de HoTT pour préciser ce que je veux dire, mais cela va sans dire qu'il en va de même pour différentes théories (typiquement la théorie des ensembles intuitionnistes qu'on utilise pour la géométrie différentielle synthétique, ou la calculabilité synthétique).
Shulman a (récemment) prouvé que HoTT avait des modèles univalents (en un sens sémantique) dans tout $(\infty,1)$-topos, en particulier cela va être vrai dans le $(\infty,1)$-topos des espaces, qui lui peut être modélisé dans ZFC (enfin on se comprend : on prend un modèle de ZFC, la quasicatégorie associée et blabla). En ce sens, oui, HoTT peut être modélisée dans ZFC, je ne crois pas avoir dit le contraire.
Par contre, tu n'as pas de modèle où tu dis naïvement type = ensemble, flèche = fonction (c'est quasiment une évidence, puisque comme tu l'as dit, deux machins isomorphes ne sont pas égaux), donc en ce sens (qui peut te paraître suspect, mais c'est le sens intuitif que je donnerais à l'expression) HoTT n'a pas de modèle dans ZFC.
Donc il faut préciser ce qu'on entend par "peut être modélisée dans".

Mais à mon sens personne n'a jamais remis en cause le premier sens (quoique, pour HoTT, c'était loin d'être une évidence, puisque ça a été prouvé cette année je crois; jusque là on n'avait pas de modèle qui faisait parfaitement tout ce qu'on voulait); et surtout je ne vois pas en quoi ça a un rapport avec ce que tu disais au dessus :-S

Mais $\bf Set$ et $\bf Cat \to \ Cat$ ont besoin d'être vues comme des catégories (les bouquins peu scrupuleux les traitent comme telles sans précision). Sinon quid d'un résultat basique comme le lemme de Yoneda?

christophe c a écrit:

Bref, évidemment que le jour où une fille ou un gars apportera un objet mathématique (je rappelle que objet mathématique se définit comme "objet égal à son illusion" pour les gens pas au courant) dont il prouvera qu'il n'existe aucun univers ZF qui le contient il recevra à la fois la MF mais aussi le prix Nobel de physique (et même peut-être aussi celui de médecine et de la paix).

Un couple $(X,f)$ où $f$ est une application injective de $X^X \to X$ et $X$ non réduit à un élément.

(NB: on ne sait pas s'il existe des univers de ZF, en revanche on sait qu'aucun univers de ZF ne contient cette chose !!!)

Où est-ce que je peux récupérer mes millions d'euros?

@foys: tu n'as pas gagné: ton truc n'existe pas et en plus la preuve que card(X) =1 est intuitionniste (sous la condition que le test d'égalité soit possible ) comme tu sais.

Mais tu essaies un truc trop fort en plus. Je ne parlais pas d'objet contradictoire mais SEULEMENT PROUVABLEMENT non dans un ZF univers. Un exemple plus pertinent : un algèbre de Boole libre ET COMPLETE à nombre infini de générateurs. Là pour le coup l'auto contradiction n'est pas claire. Mais aucune d'entre elles ne peut appartenir à un ZF univers. Par contre il reste à en prouver l'existence "ailleurs" si tu veux tes millions :-D

Je ne te prêtais pour ma part aucune intention, je voyais bien (et je vois toujours) que tu poses juste des questions. Les "gens" auxquels je fais référence (des amis de toute façon) ne viennent pas sur le forum (ou très peu).

bah il est CC-compatible mais quasi-illisible

Ah parce que tu crois franchement que si à la place de prendre des inaccessibles (ce qui fait une ligne et est propre), utiliser les usine à gaz absconses, inutiles et ubuesques issues de la certes "valide" démarche

<<est une suite d'extensions conservatives multisortes de ZFC (le premier étage étant NBG et se devant de contenir Set, et aussi la catégorie de tous les groupes et consorts).>>

l'aurait rendu lisible.

Parfois, tu m'épates dans ton ressenti de ce qui est "lisible" ;-)

De mon téléphone je voudrais resignaler le post avec un lien que j'ai mis et qui est peut être passé trop inaperçu.
http://www.les-mathematiques.net/phorum/read.php?16,1875514,1880056#msg-1880056

Pour moi ce Doc humoristique est probablement le MEILLEUR Doc qui présente sans pub excessive et avec fortes et précises informations en peu de ligne de quoi il s'agit. L'auteur semble avoir du recul et tenter de rester neutre.

Je l'ai souvent fait, et là, je suis sur mon pc (je rentre à l'instant). J'ai des lettres recommandées à taper et envoyer, et un pdf de mise au point (que je mettrai sur HAL) passera après (désolé, je dois me forcer à être un peu adulte).

Mais en résumé:

1/ Tu as des chercheurs qui taffent

2/ Tu as une erreur "congénitale" qui se transmet depuis 150ans, de bouche de druide à oreille de druide

3/ Alimenté par (2), , les (1) continuent de maquiller leur ré-invention de l'eau chaude en novations.

Concrètement, ça donne quoi?

4/ Les (1) sont des descendants de divers catégories de gens, tantôt des ancètres qui avaient très peur que les maths deviennent renommées en "logique appliquée", tantôt des jeunes voulant des postes sans résoudre de problèmes ouverts, etc, etc. Ils ont tous en commun qu'ils n'ont pas fait de logique ou pas été jusqu'au bout dans leurs études de logique (pour des raisons parfois tout à fait excusables).

5/ Ca les a conduit à continuer et prolonger, et même parfois mettre en scène la faute (2) comme une vérité.

6/ Mais l'erreur (2), c'est quoi? Bin c'est très simple: c'est la recherche de consistance.

6.1/ Je détaille un peu. La science consiste à travailler avec une langue très simple qui consiste, pour abréger à créer des définitions. Hélas, ces définitions peuvent prendre des paramètres et donc boucler. Autrement dit, tu as des a:=f(a) qui sont DIRECTEMENT PERMIS DEDUCTIVEMENT SANS AXIOME par la langue.

6.1.1/ Via $e:=\{x\mid x\in x\to 34=888\}$, tu obtiens la phrase $P:=(e\in e)$ telle que $P=(P\to (34=888))$, vérifiant :

$$ P\to ((P\to (34=888))) = (P\to (34=888)) $$

qui dupliquée deux fois, te donne finalement que $34=888$

6.1.2/ Autre exemple: la fonction $a:=(x\mapsto f(x(x)))$ est telle qu'avec $u:=a(a)$, tu as $f(u)=u$ (toute fonction a un point fixe)

6.2/ Ca s'est appelé "la crise des fondements".

6.3/ Ce n'était pas grave, mais le vent de platonisme qui existait à l'époque (on sortait tout juste de l'ère des religions et des totalitarismes résultant, on n'avait pas encore poser "toute religion est une secte" (et même aujourd'hui, ce principe clé des république pouvant marcher n'est pas vraiment bien solidifié) a fait paniquer de manière catastrophée tout le monde

6.4/ Résultat, "faute de mieux" on a typé. Ce réflexe de typer était débile car il se nourrissait à l'esprit religieux d'avant sans en être conscient, et au plus grand mépris des arguments**, pourtant immédiats, qui cassait l'initiative bisounours:

6.4.1/ "ah, msieurs-dames, vous ne pouvez pas parler de contradiction dans Q:="je suis fausse", car en fait Q n'a pas de sens, et il n'y a pas de contradiction"

6.4.2/ (la version prédicative étant "ah, msieurs-dames, vous ne pouvez pas parler de $x(x)$, car $x$ n'a pas le type des fonctions qui peuvent le prendre en argument"

**6.4.3/ "ok, bin Q:="je suis fausse ou n'ai pas de sens" "

** 6.4.4/ "ok, bin $x(x)=UNDEFINED$".

6.5/ Cette recherche de consistance, pourtant définitivement condamnée par Godel a la vie dure et a conduit de manière assez régulière des gens à produire des usines à gaz prétendument "inventives" alors qu'ils réinventent systématiquement l'eau chaude. De plus, ça conduit à remplacer bien souvent 5 lignes par 500 pages, ce qui est le comble non seulement du ridicule, mais surtout de l'arnaque, car derrière tu as des amateurs ou des jeunes aspirants qui vont parfois devoir passer une année à ingurgiter le manuel de 500 pages, ce qui produit un syndrôme de Stockholm ensuite et les amène à défendre "becs et ongles" leur souvenir de cette année sacrifiée.

7/ La réalité c'est quoi?

7.1/ Comme souvent, la physique a 100 ans d'avance (et ce n'est pas forcément dû à de la bonne volonté des physiciens), et cela fait 120ans qu'elle est confronté à une phrase égale à sa négation. (Que dis-je, à DES phrases, chacune égale à sa négation).

7.2/ L'être humain matheux non physicien en est encore à fuir à toute jambe devant une pareille bestiole, en particulier, et même scolairement et dans les écoles spécialisantes, on continue de traumatiser les élèves avec une sorte d'obligation religieuse de NE PAS APPELER ENSEMBLE les ensembles suivants:

7.2.1/ $\{x\mid x\notin x\}$
7.2.2/ $\{x\mid \forall y\in x: (y\notin y) \}$
7.2.3/ $\{x\mid x$ est bien fondé$\}$
etc, etc,

7.3/ Mais surtout, psychanalytiquement parlant, ça a le dévastateur effet de donner l'impression à ces jeunes (ou ces victimes) que ces ensembles n'existent pas. Et que $0$ est bien différent de $1$

7.4/ Or LE FAIT EST et il s'écoulera encore de nombreuses décennies avant que ça cesse, que TOUT EN AMONT, la science utilise l'égalité EN DUR suivante: $(x\mapsto expression) (a) = ReplaceByDans(x,a,expression)$

7.5/ De ce fait, les gens bottent pudiquement en touche et appelle ça "des métamaths". Bin voui, le point fixe de $f$ suivant $(x\mapsto f(x(x)))(x\mapsto f(x(x)))$ qu'est-ce que tu veux, c'est des métamaths, et ça se voit :-D :-D

7.6/ Bref, je fatigue un peu. Je termine de manière un peu expéditive.

7.7/ La réalité c'est quoi. Et bien c'est simple: $card(Monde)=1$, point barre. Faut vivre avec et c'est tout. Ou faut prendre des petites théories anecdotiques (des groupes, des anneaux, des cercles, des ensembles, HoTT, des catégories, je ne sais quoi) et travailler uniquement dedans

7.8/ Il y a cependant un point qui est incontestable et factuel, c'est LE FONDEMENT D ELA SCIENCE ET DES MATHS;

7.9/ Quel est-il?

7.10/ La réponse est simple: tout doit se voir, et ce que vous ne prouvez pas, vous le supposez.

7.11/ A ce titre, il n'y a strictement aucune raison de vouer un culte à la phrase $P=(nonP)$ générée par $e(e)$ avec

$$ e: =[x\mapsto non(x(x))] $$

puisque le chemin à parcourir quand on exécute $e(e)$ est la moitié du plus grand infini possible** et imaginable par quelqu'être vivant que ce soit dans quelque monde que ce soit, même en rêve

** celui qui permet de faire $0=1$ par exemple.

7.12/ Mais ne pas vouer un culte NE DOIT PAS VOULOIR DIRE croire à l'inexistence. Décider de croire à l'inexistance de quelque chose qu'on a sous le yeux est pour le moins "idiot".

7.13/ Le système scolaire, lui aussi, commet de très nombreuses erreurs, dont je te donne quelques exemples:

7.13.1/ Par exemple, il va maladroitement dire que l'axiome de récurrence est présenté en Terminale (alors qu'il est utilisé dès le collège et officiellement et formellement admis en première (toute série))

7.13.2/ Une pudeur déséquilibrée conduit les enseignants à commettre l''erreur d'utiliser $\iff$ plutot que $=$ pour les phrases ce qui déplatonise gratuitement l'univers mathématique au plus mauvais moment. En effet, c'est à peu près l'époque où il ne faut pas confondre un nom et sa valeur, où $7+3$ doit être compris comme étant un produit, car C'EST $10\times 1$, etc, etc. Certes, on peut débattre "gentiment" sur les abus de langage, mais le changement de signe (une phrase vit (pour l'enfant) dans $\{vrai; faux\}$, et écrire pudiquement $vrai\iff vrai$ plutôt que $vrai=vrai$ est vraiment pluss que maladroit

7.13.3/ Bref, tous les éléments précédents conduisent les ignorants à typer les choses, bon ça encore passe, mais à accuser l'ensemblisme de les typer mal (ce qui est le comble de la débilité puisque la TDE (ou le LC ce qui revient strictement au même) a comme particularité et marque de fabrique que justement rien n'est typé et tout est interne (par vocation même de parler avec des mots de tout ce qui est possible)

7.13.4/ Il suit que des gens qui , par exemple, veulent se prétendre inventifs, vont prétendre que $3\in (5\in \N)$ n'a pas de sens*** en TDE, alors qu'eux, gros malins qu'ils se revendiquent savent lui donner un sens, et sous-entendu "le bon". Ils passent donc complètement à côté du réel, et en passant ignorent assez superbement ce que fait la TDE, lui invente un typage idiot qu'elle n'a strictement jamais revendiqué pour mieux la copier, mais plus maladroitement et en réinventant l'eau chaude

*** alors que c'est faux car $(5\in \N)=\{\emptyset\}$ et $3\neq \emptyset$ (par exemple)

7.13.5/ Bref, comme autre exemple, on peut signaler comme peu connu, et manifestement pas de ces victimes de publicité mensongère, que $(2=2)(7)(19)=7$ ou que $phrase(x)=(x\subset 1)$

7.14/ Une fois de plus, je le rappelle les "connaisseurs", y compris les fans et professionnels de HoTT ne sont pas les ignorants. Leur tort n'est pas d'ignorer ce que je viens de raconter, mais de profiter de l'ignorance DES amateurs pour leur faire avaler des couleuvres. C'est pas bien :-D

7.15/ Par exemple, je ne vais apprendre ni à max, ni à GBZM, ni à un certain nombre d'autres experts que $(3=2)=\emptyset$ et que $)7=7 ) = \{1\}$. A la rigueur, je peux peut-être les informer (puisque c'est la chambre légèrement à côté) que $(8=10)(+)(11) = 11$ et encore et de toute façon ce n'est pas vraiment important.

Je ne vais pas non plus, eux, leur apporter quoique ce soit quand je les mets en garde contre la pub, pour la bonne raison qu'ils connaissent parfaitement ces systèmes donc n'ont pas besoin de moi pour les évaluer. A.Prouté, spécialiste de topologie algébrique, et de topos présente GBZM comme le meilleur spécialiste de France des topos (je ne sais plus (plutôt pas) pourquoi, mais je crois que je n'avais pas eu le temps de lui poser la question car je lui téléphonais entre 2 métros)

7.16/ Le problème est plus en ce qui concerne les amateurs. Eux croient "bêtement" qu'une proposition, une preuve, etc n'est pas un ensemble, que $2=2$ est une phrase "donc" pas un ensemble, etc, etc. Ca, à la rigueur ce n'est pas grave car on peut les détromper vite. Par contre, ils croient d'eux-mêmes, victimes de la pub, que la théorie (bêtement récursivement énumérable et POUSSIVE CAR CONSISTANTE (et en fait assez faible) HoTT) ECHAPPE à la TDE (alors qu'elle est comme tout autyre objet construite dedans), et surtout vérifie la propriété, comme je l'ai dit hier:

7.17/ Ce sur quoi je veux attirer l'attention est que cette FAUTE n'est pas faite par les experts, elle est disons juste laissé faite complaisemment par eux au titre qu'on aura ainsi plus de jeunes, plus motivés pour se spécaliser dans ce domaine

8/ Bon je m'arrête là, sans conclure. J'attends tes éventuelles questions. Si par exemple tu veux savoir pourquoi il y a de l'homotopie dans cette histoire, c'est trivial et très simple (mais ça ne t'intéresse pas forcément). Donc je préfère attendre tes questions.

9/ Je termine en me répétant: tout ceci est à peu de choses trivial dès lors que tu sors de l'obsession de consistance. Autrement dit, la faute (2) est une véritable catastrophe dans tout ce secteur de recherche.

9.1/ Corollaire de ça: sans type dire les mêmes choses prend 3 pages, avec types, c'est un manuel illisible de 500 pages. DE PLUS le fait de typer est assez illusoire, certes ça bride et on peut espérer de la consistance, mais on est comme une tente en toile légère dans la forêt vierge ce faisant, on se donne l'illusion d'être protégés par la toile de la tente, mais c'est très enfantins et inefficaces. Dès lors même que tu joues au banalités ensemblistes (consistant à se demander si $(2\in 3)\in ((30-4=2)\in (1=1))$, ce n'est pas parce que tu prétends le faire de manière typée que ça change grand chose. Formellement, tu es dans un mouvement bien connu (même si tu l'appelles homotopie pour faire le malin) dont l'origine est la TDE VERSION CDF, et le typage est bien un tente en toile légère.

On est d'accord sur notre désaccord. Remplacer $faux$ par "n'a pas de sens" fait de l'effet à certaines personnes, je respecte cet effet comme émotion, mais je le redis, opératoirement ce n'est que changer un mot.

Plus sérieusement, on a remplacé depuis longtemps $\{vrai; faux\}$ par une structure bcp plus grosse, il y a même eu une médaille Field (la seule) basée ENTIEREMENT là dessus (récompensant uniquement ça), et pas seulement par $\{vrai; faux; NoSens\}$

Rappelons de plus que la théorie des types peut être fondée complètement indépendamment de la théorie des ensembles

Ca n'a pas de sens de dire ça (au sens où c'est FAUX) et, je le dénonce non par idéologie mais parce que derrière cette affirmation "bon enfant" qui ne mange pas de pain (les experts savent que c'est de la coquetterie et s'en foutent), il y a je le rappelle des victimes "intellectuelles" qui y croient vraiment. Je sais bien ce que VEULENT DIRE les gens qui la prononcent, mais hélas elle n'est pas perçue comme ça. Pour les victimes de ça, tu leur fais croire, en la prononçant que les ensembles naifs sont des métamaths (et en fait, tout devient métamaths). Elles ne savent pas (de même ne savent pas la différence entre "il existe un univers qui contient" et "tous les univers contiennent", etc. Tu as même des profs d'université qui confondent "vrai" et "prouvable").

Essaie de te demander EN TOI MEME pourquoi tu TIENS TANT à ce que j'ai tort. Ce serait plutôt ça la bonne question.

Je rappelle pour finir que ce qu'il y a de pire dans cette esbrouffe (ce que font, comme MATHS, ces fans n'est pas de l'esbrouffe) ce sont justement le types (et non pas l'homotopie ou le fait de se demander si $(2=3) \in (5\in 6)$). Pourquoi? Et bien je le répète pour la 1326841364568ième fois: parce qu'ils sont (sans l'avouer) un cache-misère pour préserver une consistance (bien trop brutalement mise, qui généralement va limiter très fortement les développements, ou alors pas assez mise et le système va être contradictoire). Le prix à payer c'est que pour décrire 3pages de banalités, et renvoyer à d'importants théorèmes (classiques!!!) de topologie algébrique ou géométrie algébrique, tu vas taper un book ubuesque et vide de 500 pages (qui pour l'essentiel sera narcissique car ne fera que commenter la petite vie intime des programmeurs des logiciels de démonstration).

Appelle ça par un autre mot que de l'arnaque si tu veux, mais moi, je me sens libre et le droit d'appeler ça de l'arnaque. Mais c'est convival, je ne leur en veux pas.

Ce n'est qu'un style de toute façon. Ne perds pas ton temps à te demander pourquoi** j'adopte un style péremptoire mais plutôt ce que tu peux extraire d'informant pour toi.

** Si tu veux tout savoir, c'est juste que ça me rend nettement plus concis. Rien de plus.

Je me demande tout de même d'où vient cette haine délirante du typage... Ce sont des banales décorations syntaxiques, servant tout de même à préciser de quoi on parle.
On commet quel genre de crime en déclarant que
"Un type est une lettre, ou $(\mathbf X)\to \mathbf Y$ avec $\bf X,Y$ des types (parenthèses retirées si l'expression n'a qu'une seule lettre) et pour tous types $A,B,C$, $I_A$ est de type $A \to A$, $S_{A,B,C}$ est de type $(A\to B \to C) \to (A \to \to (A \to C)$, $K_{A,B}$ est de type $A\to B \to A$ et pour tous $x,y$ si $x$ est de type $A\to B$, $y$ de type $A$ alors $x(y)$ est de type $B$" ?

Pourquoi parles tu de haine délirante?

J'ai détaillé pas mal mon opinion dans ma réponse à xax. Tu vas voir que je n'ai aucune haine. J'essaie juste de protéger les novices des invitations au culte chimérique qui vient de la déification (que toi tu ne pratiques pas) du mot "type".

Connais-tu HoTT ou les topos comme je les connais? (Je ne prétends pas à l'expertise). Tu sais bien que je suis adepte de l'importance des recherches en CCH donc c'est me faire un procès injuste non?

Mais toi sais tu que par exemple le typage de HoTT est une foutaise en bonne et due forme et que pour la cacher ses promoteurs parlent de types dépendant d'un paramètre etc? Bref, as tu regardé de près et évalué la quantité de esbrouffe présente dedans? Crois tu que s'ils avaient banalement formalisé comme tout le monde et gentiment leur système au premier ordre et sans utiliser le mot type ils auraient le même succès?

Foys, toi qui es raisonnable, jette donc un oeil et reviens me dire :-D (je sais que tu vas avoir un choc). Encore une fois je ne nie enrien la présence de bonnes maths dedans. Mais évalue la proportion de com et reviens me dire :-D

Je ne pense pas connaître aussi bien que toi les détails purement techniqued concernant les raccourcis permis par HoTT en calcul de groupes d'homotopie, mais je pense avoir suffisamment cerné HoTT (qui n'est rien d'autre qu'un fragment de TDE avec des balises prétentieusement nommées) pour parier que même dans 2 ans tout expert passant sur le présent fil ne pourra pas nier un seul des trucs que j'ai dits.

Maintenant comme tu le dis souvent, singer les ordres superieurs avec des mots et algos de réécriture c'est bien ou pas bien selon l'OPINION des gens.

Pour moi c'est pas bien je le répète PARCE QUE J'AI VU DE MES YEUX les.victimes de ces faux espoirs. Regarde 708 par exemple qui signale avec émotion que in est remplacé par ":". Ou même TOI MEME qui me réponds à côté en croyant que HoTT n'est pas véritable au premier ordre. (Je rappelle que TOUTE THEORIE récursivement enumerable est au premier ordre, et pour celles comme ZF ou HoTT c'est même trivial).

Je pense qu'il faut faire attention à la pub. L'aitre jour je ne sais plus qui avait même confondu la syntaxe et singeage du second ordre au premier ordre avec le vrai second ordre (ie le plein).

Je viens de lire un article de Chambéry Loir (un matheux optimiste) qui dit "j'ai rien compris mais qu'est ce que ça a l'air beau". Bon après si mes alertes tue l'amour ne dont pas écoutées tant pis, c'est pas grave. Mais à tout enfumer comme ça, je pense qu'on risque de grosses pertes. Certaines découvertes et expertises sont fragiles. Ré inventer l'eau chaude (l'univalence est connue et banalement utilisée depuis lgtps ne serait ce que par moi même mais en logique et informatique, et onn' a pas envoyé des VRP la vendre sur tous les marchés) peut conduire à fermer tous les anciens robinets d'eau chaude.

Bah en attendant tu n'as pas répondu à mon "défi" :-D et je ne pense pas que ce soit si simple...

Après, attention, ce ne sont largement pas 98% du manuel qui sont théorie de la dem et CCH. D'ailleurs il n'y a rien là-dessus dans le manuel. Je viens de jeter un oeil: il y a 100 pages (donc 1/5) sur théorie de l'homotopie et catégories, 80 sur la reconstruction des "maths usuelles" : tde et réels et au début 250 sur la présentation/les bases de la HoTT , où on explique les higher inductive types notamment, mais aussi le concept de $n$-types etc. L'apparat de théorie des types formelle est en appendice, et représente une très faible partie du bouquin.

"l'univalence est connue et banalement utilisée" : faudra que tu m'expliques alors pourquoi quelques messages plus haut tu disais que c'était une "faute scientifique" d'essayer de l'avoir :-S

@max: je n'avais tout simplement pas lu la ligne où tu me défies d'écrire HoTT au premier ordre. Bin je te réponds qu'il l'est déjà, que veux-tu que je fasse. Ce n'est pas parce qu'on dit (mince, je sens que je vais dire un truc proche du général de Gaulle, mais je ne sais plus quoi) "deuxième ordre, troisième ordre, etc) que ce n'est pas du premier ordre. ZF (dans quoi est écrit HoTT est DEJA lui-même du premier ordre. Que veux-tu que je fasse: que je change le mot "constructureur" en un autre mot pour enlever l'odeur d'informatique ou de subtilité? Précise. Moi je veux bien remplacer "higher inductive type" par un mot plus modeste, je ne vois pas tellement en quoi je vais t'apporter quelque chose que tu sais déjà, qui n'est rien d'autre que le fait que toute théorie s'écrit au premier ordre (et même avec un nombre fini d'axiomes quand elle est récursivement énumérable)

A moins qu'on ne parle pas de la même chose...

@708: en quoi penses-tu que remplacer $\in$ par $:$, ou, si tu préfères, en remettant $\in$ à la place de $:$ partout dans HoTT va changer quelque chose?

J'en profite pour illustrer le côté pub. C'est un peu méchant, mais très fidèle. Voici 2 vidéos:

1/ un jeune homme bénévole qui fait ça pour son plaisir nous fait la pub de l'axiome d'univalence:


2/ Un médecin pas bénévole nous fait le pub de sa gélule:


Pardon, mais où sont les différences fondamentales, en dehors du bénévolat?

Et en quoi dans l'une comme dans l'autre, on apprend quelque chose de tangible?