Jean Abou Samra
@jeanas.bsky.social
PhD student in theoretical computer science at Eötvös Loránd University in Budapest. Mainly here to chat about TCS/math.
(I meant “factor through true : 1 → Ω”.)
November 25, 2025 at 8:57 AM
(I meant “factor through true : 1 → Ω”.)
I think the stupid trick is this:
Assuming p(x) ⊢ q(x), apply the definition to the subobject ι : {x ∈ X | p(x)} ↪ X. Certainly the map p ◦ ι : {x ∈ X | p(x)} ↪ X → Ω will factor through 1. So q ◦ ι : {x ∈ X | p(x)} ↪ X → Ω will also factor through 1 and we can work from there.
Assuming p(x) ⊢ q(x), apply the definition to the subobject ι : {x ∈ X | p(x)} ↪ X. Certainly the map p ◦ ι : {x ∈ X | p(x)} ↪ X → Ω will factor through 1. So q ◦ ι : {x ∈ X | p(x)} ↪ X → Ω will also factor through 1 and we can work from there.
November 25, 2025 at 7:28 AM
I think the stupid trick is this:
Assuming p(x) ⊢ q(x), apply the definition to the subobject ι : {x ∈ X | p(x)} ↪ X. Certainly the map p ◦ ι : {x ∈ X | p(x)} ↪ X → Ω will factor through 1. So q ◦ ι : {x ∈ X | p(x)} ↪ X → Ω will also factor through 1 and we can work from there.
Assuming p(x) ⊢ q(x), apply the definition to the subobject ι : {x ∈ X | p(x)} ↪ X. Certainly the map p ◦ ι : {x ∈ X | p(x)} ↪ X → Ω will factor through 1. So q ◦ ι : {x ∈ X | p(x)} ↪ X → Ω will also factor through 1 and we can work from there.
Oh and by the way, Lambek & Scott disagree with your characterization of the theorem as “nontrivial”. This is all they have to say about the proof:
November 24, 2025 at 10:15 PM
Oh and by the way, Lambek & Scott disagree with your characterization of the theorem as “nontrivial”. This is all they have to say about the proof:
Offhand I don't actually recall seeing a topos theory book written in the past 15 years. I do have some lecture notes like those by Jaap van Oosten. They're quite tough to follow but still more to my taste.
November 24, 2025 at 9:53 PM
Offhand I don't actually recall seeing a topos theory book written in the past 15 years. I do have some lecture notes like those by Jaap van Oosten. They're quite tough to follow but still more to my taste.
And a contrario, there are things that they make overly minimalistic (perhaps shorter but less natural): using impredicative encodings seems really useless to me (it's like defining groups by axiomatizing division instead of product — is there a single theorem that this helps prove?).
November 24, 2025 at 9:49 PM
And a contrario, there are things that they make overly minimalistic (perhaps shorter but less natural): using impredicative encodings seems really useless to me (it's like defining groups by axiomatizing division instead of product — is there a single theorem that this helps prove?).
No idea why all those old topos theory books, and especially this one, complicate this definition so much.
November 24, 2025 at 9:40 PM
No idea why all those old topos theory books, and especially this one, complicate this definition so much.
Especially since they've just spent so many pages on cartesian closed categories and satisfaction in a topos can (I'm pretty sure) be defined by just reusing the cartesian closed structure (the topos structure just gives you some extra distinguished objects and morphisms).
November 24, 2025 at 9:40 PM
Especially since they've just spent so many pages on cartesian closed categories and satisfaction in a topos can (I'm pretty sure) be defined by just reusing the cartesian closed structure (the topos structure just gives you some extra distinguished objects and morphisms).
I can imagine how this characterization might be useful as a theorem, but it strikes me as really odd to choose it as the definition.
November 24, 2025 at 9:37 PM
I can imagine how this characterization might be useful as a theorem, but it strikes me as really odd to choose it as the definition.
Oh I think I see why it works. But everything in this book is so weirdly presented…
November 24, 2025 at 6:51 PM
Oh I think I see why it works. But everything in this book is so weirdly presented…
Quand je vois que ceci était la une du « Figaro » hier, je me demande si ce moment n'est pas déjà arrivé, en fait.
November 23, 2025 at 9:54 PM
Quand je vois que ceci était la une du « Figaro » hier, je me demande si ce moment n'est pas déjà arrivé, en fait.
Enjoy 🤓
(yes, @gro-tsen.bsky.social, I know you're going to react with some combination of 🙄, 😫 and 😱 by emoji kitchen 😉)
(yes, @gro-tsen.bsky.social, I know you're going to react with some combination of 🙄, 😫 and 😱 by emoji kitchen 😉)
November 21, 2025 at 11:12 PM
Enjoy 🤓
(yes, @gro-tsen.bsky.social, I know you're going to react with some combination of 🙄, 😫 and 😱 by emoji kitchen 😉)
(yes, @gro-tsen.bsky.social, I know you're going to react with some combination of 🙄, 😫 and 😱 by emoji kitchen 😉)
La presse en parle : www.lemonde.fr/pixels/artic...
L’enquête sur la plateforme X étendue à des « propos négationnistes » publiés par son IA, Grok
Dans la publication visée, qui fait aussi l’objet de plaintes de la Ligue des droits de l’homme et de SOS Racisme, Grok affirme notamment que les chambres à gaz du camp d’extermination nazi d’Auschwit...
www.lemonde.fr
November 19, 2025 at 6:58 PM
La presse en parle : www.lemonde.fr/pixels/artic...
et normal est dénombrablement paracompact, avant d'enchaîner sur le fait que tout de même, il y a quelques implications de base que tout mathématicien devrait connaître, comme le fait que tout espace T₁ pseudonormal est régulier (quelque chose de ce genre).
November 16, 2025 at 1:00 PM
et normal est dénombrablement paracompact, avant d'enchaîner sur le fait que tout de même, il y a quelques implications de base que tout mathématicien devrait connaître, comme le fait que tout espace T₁ pseudonormal est régulier (quelque chose de ce genre).
J'ai récemment ouvert un bouquin de topologie, que je ne retrouve malheureusement pas, dans la préface duquel l'auteur se plaignait que la « botanique » des espaces topologiques était souvent portée à l'excès et qu'on se fichait vraiment de savoir si tout espace dénombrablement métacompact …
November 16, 2025 at 1:00 PM
J'ai récemment ouvert un bouquin de topologie, que je ne retrouve malheureusement pas, dans la préface duquel l'auteur se plaignait que la « botanique » des espaces topologiques était souvent portée à l'excès et qu'on se fichait vraiment de savoir si tout espace dénombrablement métacompact …
Oui, ça s'appelle les maths synthétiques, et c'est un sujet de recherche actif et très intéressant. Et toute personne qui a fait des maths dans le supérieur a très probablement déjà rencontré ce type d'approche : qui a commencé l'analyse avec une construction des nombres réels ?
November 16, 2025 at 11:11 AM
Oui, ça s'appelle les maths synthétiques, et c'est un sujet de recherche actif et très intéressant. Et toute personne qui a fait des maths dans le supérieur a très probablement déjà rencontré ce type d'approche : qui a commencé l'analyse avec une construction des nombres réels ?
C'est quoi, par curiosité ?
November 14, 2025 at 4:12 PM
C'est quoi, par curiosité ?
I actually spent most of the time doing an informal introduction to realizability since the audience was not familiar with it. In case this interests anyone, the slides are here:
jean.abou-samra.fr/talks/2025-1...
jean.abou-samra.fr/talks/2025-1...
jean.abou-samra.fr
November 10, 2025 at 10:32 PM
I actually spent most of the time doing an informal introduction to realizability since the audience was not familiar with it. In case this interests anyone, the slides are here:
jean.abou-samra.fr/talks/2025-1...
jean.abou-samra.fr/talks/2025-1...
C'est sans doute un peu extrême mais personnellement, depuis quelques versions de Fedora (qui arrivent tous les 6 mois), je réinstalle complètement plutôt que de mettre à jour. L'intérêt est surtout de vérifier que les sauvegardes que j'ai suffisent à tout remettre en ordre en cas de pépin.
November 9, 2025 at 2:59 PM
C'est sans doute un peu extrême mais personnellement, depuis quelques versions de Fedora (qui arrivent tous les 6 mois), je réinstalle complètement plutôt que de mettre à jour. L'intérêt est surtout de vérifier que les sauvegardes que j'ai suffisent à tout remettre en ordre en cas de pépin.