<foo> simply produces <foo>in the text).
<URL: http://somewhere.tld/ >,
and it will be automatically made into a link.
(Do not try any other way or it might count as an attempt to spam.)mailto: URI,
e.g. mailto:my.email@somewhere.tld,
if you do not have a genuine Web site).
jeanas (2025-12-28T07:49:22Z)
Facepalm. Bon, on va dire que j'étais encore convalescent en écrivant le commentaire précédent.
Ruxor (2025-12-27T18:23:52Z)
@jeanas: Si, dans le topos effectif, les réels de Dedekind, qui coïncident avec les réels de Cauchy ou de Cauchy modulés, sont (isomorphes à) une assemblée (van Oosten, “Realizability”, propositions 3.2.15 et 3.2.16) : c'est par exemple l'assemblée portée par l'ensemble des réels calculables et où l'ensemble E(x) des réalisateurs de x, si x est un tel réel, est l'ensemble des codes de suites calculables de rationnels convergeant de façon explicite vers x. C'est aussi une conséquence du fait que les réels sont (¬¬)-séparés et que les assemblées sont, à isomorphisme près, exactement les objets (¬¬)-séparés du topos effectif. Les coupures de MacNeille sont aussi une assemblée, et c'est aussi instructif de voir comment : si je ne m'abuse c'est l'assemblée portée par l'ensemble des réels (du monde classique ambiant) et où E(x) est l'ensemble des couples de rationnels (s,t) qui encadrent x (je veux dire, s<x<t). (Quant aux réels singletons, ce sont ceux pour lesquels x s'avère être un réel calculable.)
(C'est le genre d'exemples que j'ai bien envie de mettre dans un bouquin.)
jeanas (2025-12-27T14:06:30Z)
Tu as peut-être raison, enfin il faudrait que je vérifie ça soigneusement. J'ai appris par James Hanson <URL:https://mathoverflow.net/a/484638/519112> que ZF ne peut pas construire tous les types quotient-inductifs par un résultat d'Andreas Blass (« Words, free algebras, and coequalizers », Fundamenta Mathematicae 1983 volume 117 no 2), et c'est donc un exemple (il y en a quelques autres) où HoTT permet de faire plus de choses constructivement. Mais ça ne s'applique peut-être pas à ce cas particulier. Je note tout de même que la construction du HoTT book est prédicative et donc devrait marcher dans le modèle des assemblées cubiques, ce qui est un peu surprenant vu qu'aucune sorte des réels que tu définis ne va être une assemblée dans le topos effectif. Mais là je suis vraiment en terrain inconnu et je n'ai pas envie d'y réfléchir pour le moment. J'arrête donc de t'emmerder :-)
Ruxor (2025-12-26T12:05:59Z)
@jeanas: Comme d'habitude, la page que tu lies pourrait être écrite en chinois pour ce que j'en comprends. Mais le peu que j'en comprends suggère que, modulo subtilités qui m'échappent totalement quant aux types homotopiques, l'ensemble en question est simplement la clôture (dans les réels de Dedekind) des rationnels par limites de suites de Cauchy ou plus probablement par limites de suites de Cauchy modulées. Si c'est juste, je me demande pourquoi ce n'est pas dit, mais en tout cas j'appelle ça quelque chose comme « la clôture de Cauchy (modulée ?) des rationnels ».
Je ne sais pas si ces notions de clôture ont vraiment un intérêt. Dans ZF classique, par exemple, où on ne peut plus affirmer qu'une réunion dénombrable d'ensembles dénombrables est dénombrable, on pourrait très bien étudier les ensembles qui sont égaux à la clôture de leurs singletons par l'opération de réunion dénombrable : vu que cette notion a été tellement peu étudiée qu'elle n'a même pas reçu un nom, je soupçonne qu'elle n'est pas franchement passionnante, et qu'il en va de même, et pour les mêmes raisons, de la notion de clôture de Cauchy. (Mais j'en dis un mot dans la partie 4.)
jeanas (2025-12-25T18:13:45Z)
Comme je sais qu'a priori tu n'aimes pas HoTT, je ne m'étends pas, mais il est intéressant de noter que dans ce contexte, il existe une construction à la Cauchy des réels pour laquelle on peut prouver que les réels sont Cauchy-complets de manière purement constructive, sans recourir à l'axiome du choix dénombrable. <URL:https://ncatlab.org/nlab/show/HoTT+book+real+number>