Remote

Josselin Poiret

@jpoiret@types.pl

mastodon 4.7.0-alpha.2+glitch

types and categories and algebra and geometry and free software

i use guix btw

avatar: cover art of Love is a Stream by Jefre Cantu-Ledesma

background picture by @VojtechStep@mathstodon.xyz

0 Followers

0 Following

12 Posts

Joined February 24, 2023

stalk me at:

https://jpoiret.xyz

gpg:

39248CD841C63CC336DCAF2F505E40B916171A8A

Posts

Josselin Poiret @jpoiret@types.pl · May 09, 2026

Replying to @mc@mathstodon.xyz

@mc@mathstodon.xyz unless the accompanying paper is well-written and has interesting insights, I would say no

Josselin Poiret @jpoiret@types.pl · May 05, 2026

Replying to @JacquesC2@types.pl

@JacquesC2 i don't think the author version would include any proof whatsoever then

Josselin Poiret @jpoiret@types.pl · May 05, 2026

Replying to @juliengossa@social.sciences.re

@juliengossa@social.sciences.re beaucoup de sportifs ne vivent pas non plus de leur pratique, et une médaille représente souvent un gain financier conséquent. Je ne pense pas qu'on puisse dire que c'est "bien pire", c'est juste comparable.

Josselin Poiret @jpoiret@types.pl · Apr 28, 2026

me when the stochastic machine reinforces my beliefs

Josselin Poiret @jpoiret@types.pl · Apr 27, 2026

Replying to @jonmsterling@mathstodon.xyz

@jonmsterling @carloangiuli oops, i guess it's getting late and i misread the word! In any case, I'm very much intensionally-minded: while you can't distinguish extensionally equal functions internally, when i prove that two functions are equal I do mean to say that they are implemented in the same way. Otherwise I would be proving that they are extensionally equal. If you add funext, this distinction isn't possible anymore, which mean you trade nuance for convenience. Don't get me wrong, convenience can be very nice, but I also like having this precise tool for specific applications!

Josselin Poiret @jpoiret@types.pl · Apr 27, 2026

Replying to @carloangiuli@mathstodon.xyz

@carloangiuli @jonmsterling count me in the "funext isn't natural" camp 😈

Josselin Poiret @jpoiret@types.pl · Apr 05, 2026

Replying to @jpoiret@types.pl

@sophiehuiberts@mathstodon.xyz small mistake on my part, \@currentcounter is LaTeX, not TeX

Josselin Poiret @jpoiret@types.pl · Apr 05, 2026

Replying to @sophiehuiberts@mathstodon.xyz

@sophiehuiberts@mathstodon.xyz I guess you are numbering your lemmas with the same counter as your theorems? Most packages that do “clever” things with references in TeX use the “reference counter name” \@currentcounter to infer additional information, but if you share counters between environments that won't be enough. There is a section specifically about how to make it work with lemmas (with code) in the zref-clever manual section 10.2, look for the “shared counter” paragraph. The idea is that you locally change the inferred meaning of the theorem counter in lemma environments.