@jeanas@mathstodon.xyz

Jean Abou Samra (new account) @jeanas@mathstodon.xyz · Jul 11, 2026

Replying to @MartinEscardo@mathstodon.xyz

I don't think I know what this means for the future, and I don't think anybody else knows either.

Some of the consequences of the current race to build data centers as fast as possible before we switch to a fully clean grid are unfortunately very well-predicted: just open the IPCC reports :(

3

0

Jean Abou Samra (new account) @jeanas@mathstodon.xyz · May 31, 2026

I have in my mind two conflicting definitions of “f : X → Y has the Baire property (BP)”. (X and Y are topological spaces which I'm happy to assume Polish.) The first is that the preimage of an open subset has the BP (coincides with an open modulo a meager, and open can be replaced with Borel here). The second is that f is “Baire-measurable”, i.e., measurable with respect to the σ-algebras of BP subsets: the preimage of a BP has the BP. Did I dream up that these are equivalent? It comes down to showing that if the preimage of an open has the BP, then the preimage of a nowhere dense has the BP, but I'm stuck on that.

0

Jean Abou Samra (new account) @jeanas@mathstodon.xyz · May 28, 2026

The setoid model translation takes a model of type theory and returns a new model which validates function extensionality and propositional extensionality for SProp. Has anyone already worked out something like this for unique choice? I guess something like replacing functions with functional relations should work, right? I'm asking because I understand unique choice to be the reason why the definition of the effective topos is so complicated and doesn't just use plain setoids (see the last page of https://arxiv.org/pdf/1307.3832).

1

3

1

0

Jean Abou Samra (new account) @jeanas@mathstodon.xyz · May 27, 2026

Here's a question I've meant to ask for a long time: https://mathoverflow.net/q/511737/

2

0

Jean Abou Samra (new account) @jeanas@mathstodon.xyz · May 25, 2026

I added a definition of the effective topos to Wikipedia. I think it's incomprehensible for a newcomer (as it was to me two years ago), but since I ran out of time, pedagogy will have to wait for later or someone else.

https://en.wikipedia.org/wiki/Effective_topos#Definition

2

0

Jean Abou Samra (new account) @jeanas@mathstodon.xyz · May 22, 2026

The Budapest type theory group is hiring a postdoc to work on higher observational type theory.

http://lists.seas.upenn.edu/pipermail/types-announce/2026/012535.html

8

1

21

0

Jean Abou Samra (new account) @jeanas@mathstodon.xyz · May 12, 2026

Replying to @totbwf@types.pl

@totbwf@types.pl @ncf@types.pl By the way, how technically feasible would it be to make Mikan translate pattern matching and recursion to eliminators?

0

2

0

Jean Abou Samra (new account) @jeanas@mathstodon.xyz · May 09, 2026

Replying to @matematiflo@mathstodon.xyz

@matematiflo@mathstodon.xyz @de_Jong_Tom@mathstodon.xyz @mevenlennonbertrand@lipn.info This looks cool. Do you know how much background will be assumed for Felix Cherubini's synthetic algebraic geometry course? Can I expect to be able to follow, as someone who's familiar with homotopy type theory but not as much as I would like with its semantics, and who knows a few basic facts of algebraic geometry at the level of varieties but doesn't know a thing about schemes?

0

2

0

Jean Abou Samra (new account) @jeanas@mathstodon.xyz · May 06, 2026

Replying to @iblech@mathstodon.xyz

@iblech@mathstodon.xyz Yes, this is precisely what made me smile :-)

1

0

Jean Abou Samra (new account) @jeanas@mathstodon.xyz · May 05, 2026

Replying to @amy@types.pl

@amy @ncf @totbwf This is great news. If I have wishes for changes that the backwards compatibility break would make possible, where should I send them?

2

1

0

Jean Abou Samra (new account) @jeanas@mathstodon.xyz · Apr 29, 2026

Replying to @jonmsterling@mathstodon.xyz

@jonmsterling I guess I'm illiterate since I often do this sort of silly typo. But more funnily:

1

0

Jean Abou Samra (new account) @jeanas@mathstodon.xyz · Apr 29, 2026

Replying to @MonniauxD@social.sciences.re

@MonniauxD (Lien cassé)

0

1

0

Jean Abou Samra (new account) @jeanas@mathstodon.xyz · Apr 28, 2026

Replying to @olynch@mathstodon.xyz

@olynch@mathstodon.xyz Does this answer your question? https://ncatlab.org/nlab/show/Yoneda+embedding#ReferencesNotation

1

2

0

Jean Abou Samra (new account) @jeanas@mathstodon.xyz · Apr 28, 2026

I'm taking a descriptive set theory course. I'm the only one from the type theory group (which is in the CS department), the others are master's students in the math department. In today's exercise session, one of them wrote on the board “{F ∈ ℱ(X) | F ∩ U}” and said that F ∩ U was a shorthand notation for “F intersects U”. Others started to laugh. He said that after all it makes sense because you can convert a set to a boolean through the function that maps the empty set to the boolean false and non-empty sets to true. After some more amusement, he continued the exercise. I didn't say anything.

4

2

0

Jean Abou Samra (new account) @jeanas@mathstodon.xyz · Apr 28, 2026

Replying to @jeanas@mathstodon.xyz

@jonmsterling Or did you mean congruence of definitional equality and specifically the xi rule / conversion under lambda? Pédrot's paper achieves it, unlike previous attempts. @mevenlennonbertrand @jpoiret @carloangiuli

4

0

Jean Abou Samra (new account) @jeanas@mathstodon.xyz · Apr 28, 2026

Replying to @jonmsterling@mathstodon.xyz

@jonmsterling Wait, what's the problem with congruence of equality? https://www.xn--pdrot-bsa.fr/articles/quotett.pdf does have the J eliminator, no? @mevenlennonbertrand @jpoiret @carloangiuli

1

3

0

Jean Abou Samra (new account) @jeanas@mathstodon.xyz · Apr 27, 2026

Replying to @jonmsterling@mathstodon.xyz

@jonmsterling What do you mean by a “combinatorial presentation of the type theory”? @MartinEscardo @carloangiuli

0

2

0

Jean Abou Samra (new account) @jeanas@mathstodon.xyz · Apr 25, 2026

Replying to @jhostert@mathstodon.xyz

@jhostert The underlying mathematical objects being manipulated are (a specific variety of) cubical sets. But I can't explain much more since one of my purposes in starting this page is to force myself to (belatedly, given my PhD topic) understand the syntax and semantics of cubical type theory sufficiently well to be able to explain this… At any rate, I think that the HoTT book is still the best place to learn about the “types as spaces” interpretation; it will be much easier to understand cubical type theory if you first have a working understanding of the HoTT book (one may hope that eventually there will be introductions to cubical type theory that don't presuppose this knowledge, but that's how it is at the moment).

1

0

Jean Abou Samra (new account) @jeanas@mathstodon.xyz · Apr 24, 2026

I also proposed to merge “Homotopy type theory” and “Univalent foundations”. Opinions are welcome on which name to retain…

https://en.wikipedia.org/wiki/Wikipedia:Articles_for_deletion/Homotopy_type_theory

1

0

Jean Abou Samra (new account) @jeanas@mathstodon.xyz · Apr 24, 2026

I just created a Wikipedia page about cubical type theory. For now this is a stub with just keyword-dropping and reference-dropping. Help to augment it is very welcome, we really need a readable first introduction to cubical type theory written down somewhere.

https://en.wikipedia.org/wiki/Cubical_type_theory

8

3

2

0

Jean Abou Samra (new account) @jeanas@mathstodon.xyz · Apr 21, 2026

Replying to @MonniauxD@social.sciences.re

@MonniauxD Non, elle est complètement différente. Les commandes sont écrites sans \ et reconnues au fait qu'elles font plus d'un caractère, et leurs noms sont souvent différents, donc par exemple $forall x, P(x) and Q(x)$ au lieu de $\forall x, P(x) \land Q(x)$. En contrepartie, on n'écrit pas $xyz = 1$ mais $x y z = 1$. De plus, il y a beaucoup plus de raccourcis syntaxiques ASCII. Par exemple, $forall x in RR, x != 0 => exists y in RR, x y = 1$ au lieu de $\forall x \in \mathbb{R}, x \neq 0 \implies \exists y \in \mathbb{R}, xy = 1$.

2

0

Jean Abou Samra (new account) @jeanas@mathstodon.xyz · Apr 19, 2026

Breaking mathematical news: recent events have formally disproved the claim that adults are adults, refuting a nearly 350 years old conjecture of Leibniz. This is the first fully automated contribution to mathematics by autonomous geopolitical agents.

4

0

Jean Abou Samra (new account) @jeanas@mathstodon.xyz · Apr 19, 2026

Replying to @jeanas@mathstodon.xyz

(Just in case anybody got misled, this was a pun.)

1

0

Jean Abou Samra (new account) @jeanas@mathstodon.xyz · Apr 18, 2026

Replying to @ncf@types.pl

@ncf By “relation”, do you mean a mere relation or a proof-relevant relation?

0

2

0

Jean Abou Samra (new account) @jeanas@mathstodon.xyz · Apr 18, 2026

In French mathematics, families are tied into tribes living on separated spaces.

2

1

0

Jean Abou Samra (new account) @jeanas@mathstodon.xyz · Apr 17, 2026

Replying to @MadameMollette@piaille.fr

@MadameMollette @bmichel D'après Le Monde https://www.lemonde.fr/politique/article/2026/04/17/sebastien-lecornu-annonce-que-les-boulangers-et-les-fleuristes-pouront-ouvrir-le-1er-mai_6680879_823448.html , il prévoit bien de déposer un projet de loi avant le 1er mai pour remplacer la proposition de loi avortée (restreint cette fois aux boulangers et fleuristes, la proposition de loi d'Attal s'appliquait à d'autres professions), mais il ne compte pas que ce projet de loi puisse s'appliquer pour ce 1er mai. Je crois que l'échéance « avant le 1er mai » est juste une manière de dire « bientôt » sans lien avec l'objet du débat. Par ailleurs, il a effectivement déclaré que « des instructions [seront données afin que] les artisans de ces deux secteurs ne souffrent d’aucune conséquence d’une ouverture le 1er mai 2026 dans les règles fixées par la future loi » et le ministre du travail a clairement dit que les consignes « consistent à ce que les commerçants, le cas échéant, n’aient pas à payer d’amende ».

0

1

4

0

Jean Abou Samra (new account) @jeanas@mathstodon.xyz · Mar 27, 2026

I just signed the “No free view? No review!" pledge to refuse reviewing papers for closed-access venues, and I encourage all researchers to do the same.

https://nofreeviewnoreview.org

89

0

63

0

Jean Abou Samra (new account) @jeanas@mathstodon.xyz · Mar 23, 2026

Replying to @highergeometer@mathstodon.xyz

@highergeometer I would love to hear some extremely elementary ∞-category theory. This seems to be a subject in which people rarely explain their intuitions in writing (e.g., why do we define a simplicial set or whichever kind of cubical set exactly like this?).

1

2

0

Jean Abou Samra (new account) @jeanas@mathstodon.xyz · Mar 02, 2026

Replying to @mevenlennonbertrand@lipn.info

@mevenlennonbertrand@lipn.info My god… Here's the thread for the record: https://rocq-prover.zulipchat.com/#narrow/channel/237977-Rocq-users/topic/Proof.20of.20false.20found.20by.20Opus.204.2E6.20and.20mxdys.20.28bbchallenge.29/with/576655078

2

1

0

Jean Abou Samra (new account)

Posts

Remote instance