3,570 reputation
1332
bio website peterlefanulumsdaine.com
location Stockholm, Sweden
age 32
visits member for 5 years, 3 months
seen 6 hours ago

Mathematician, math.LO/math.CT, currently postdoc at Stockholm University. Mainly working in categorical logic, especially homotopy type theory and higher categories.

Previously worked at Institute for Advanced Study, Princeton; Dalhousie University, Halifax, Nova Scotia; and Carnegie Mellon University, Pittsburgh.


1d
comment Injecting premises into two implicational premises connected by a tensor (multiplicative conjunction) in linear logic
Presentations of linear logic vary a bit; can you give a reference for what you are using? A rough answer: your approach sounds correct to me. It is not possible to get either one of $(A \multimap B)$ or $(C \multimap D)$ individually, but (in the presentations I know) inverting the tensor gives you the two of them together as formulas on the left of the $\vdash$, and you can then apply them to premises (1) and (2) as you describe. Some presentations may present this slightly differently, but something like this should always work.
Mar
24
comment About the proof of the proposition “there exists irrational numbers a, b such that a^b is rational”
@AndrejBauer: remember that MathOverflow had a slightly wider remit in 2011; I suspect that if this were asked today, it would get migrated to math.stackexchange.
Mar
23
comment Is there a natural bijection from $\mathbb{N}$ to $\mathbb{Q}$?
Incidentally, this sequence representation is nicely related to the one underlying Calkin-Wilf. This representation obtains positive rationals using the operations $a$, “add one”, and $i$, “add one, then invert”; Calkin-Wilf instead uses $a$ together with $j$, “invert, then add one, then invert”. These satisfy identities $i(a(x)) = j(i(x))$, $i(i(x)) = j(a(x))$. So one can convert from this representation to Calkin-Wilf by crawling from the outside in: e.g. $2/5 = i(a(i(1)) = j(i(i(1)) = j(j(a(1))$. In particular, these two representations of a rational always have the same length.
Mar
23
comment Is there a natural bijection from $\mathbb{N}$ to $\mathbb{Q}$?
@VladimirDotsenko: yes, I absolutely agree that your details are good to give, and important for a full proof. But it is often helpful to have a higher-level explanation as well as the details.
Mar
23
comment Is there a natural bijection from $\mathbb{N}$ to $\mathbb{Q}$?
The proof can perhaps be presented a bit more conceptually. Uniqueness of continued fraction forms is easily seen to be equivalent to the statement that each non-negative rational is uniquely reachable, starting from 0, by some sequence of the two operations “add 1”, or “add 1 and invert”. This gives a bijection between non-negative rationals and binary sequences. On the other hand, the usual binary representation gives a bijection between binary sequences and non-negative integers. The function $f$ is the composite of these two bijections.
Mar
17
comment What are some examples of colorful language in serious mathematics papers?
@darijgrinberg: commenting to alert that the image link in this answer seems currently dead.
Mar
16
comment project limit on $n$- simplical complex which is principal homogeneous with respect to an action
The title is currently not very descriptive — this question might get more attention if you put a few more details into the title.
Mar
15
comment Parodies of abstruse mathematical writing
From Peter Johnstone’s review of Paul Taylor’s Practical Foundations of Mathematics: “Nearly 30 years later, Paul Taylor has finally written the book of which Mathematics Made Difficult was a parody.” (It’s actually a favourable a review, and a fun book, if idiosyncratic.)
Mar
10
comment Numbers greater than Skewes's whose existence can be found in number theoretic proofs
In case it’s not clear why this answer is getting down-voted: the question specifically asks for large numbers coming from work in number theory. Graham’s Number arose from work in combinatorics, not number theory.
Mar
2
comment Adding sets not containing arithmetic progressions of length three by forcing
Just as a side remark: the machinery of forcing seems like overkill here. Suppose your question is answered positively, say by some construction sending $(s,N)$ to $(f(s),N+1)$. Then just start with $s_0 = \emptyset$, and iterate $f$ from $(s_0,0)$ to get a sequence of conditions $(s_n, n)$; now $S = \bigcup_n s_n$ gives a counterexample to Erdos-Turan.
Jan
6
awarded  Nice Question
Jan
5
answered Theorem versus Proposition
Jan
5
comment How to refer to plural of mathematical symbols - with or without an apostrophe
@YemonChoi: very good point; and the answers/discussion so far bear it out. You’ve converted me to the close-vote camp, though as “primarily opinion-based” rather than “off-topic”.
Jan
5
comment How to refer to plural of mathematical symbols - with or without an apostrophe
@YemonChoi: for PDE’s vs. PDEs, it’s certainly a general English usage question — and indeed it’s already asked and well-answered on english.stackexchange. But for $x_i$ vs. $x_i$s vs. $x_i$’s, the usage and conventions are pretty specific to mathematical writing, so it seems reasonably on-topic here to me.
Jan
5
comment Has anyone read/debunked Yessenin-Volpin–Hennix “Beware of the Gödel-Wette paradox”?
@AsafKaragila: Sure, I don’t particularly want to do it myself either, hence asking if someone already has. But when cranks accuse mathematicians of being hidebound reactionaries ignoring their work, we say that no, there are clear standards of correctness that they fail to live up to. And to substantiate this, we need (as a community) to give attention from time to time to some of the more coherent “outsider” papers, and show how they are in error. (And occasionally we may find that they’re not — though, again, I highly doubt that in this case.)
Jan
5
comment How to refer to plural of mathematical symbols - with or without an apostrophe
@YuichiroFujiwara (continuing the possibly unnecessary seriousness): A less prescriptivist approach is exactly what I’m trying to advocate! I believe that in speech, the explicitly-pluralised-with-a-[z]-phoneme version is more common/natural than the zero-pluralised version (it’s at least a common choice), and so saying “you can’t write that, because it looks terrible” (or “…is wrong”) is an unreasonably prescriptive stance. Unless you read the zero-pluralised written form as representing the explicitly-pluralised spoken form — but I don’t think most people read it that way.
Jan
5
comment How to refer to plural of mathematical symbols - with or without an apostrophe
@YuichiroFujiwara: sure, yes. I’m not advocating spelling reforms. But when there are multiple existing conventions (as in this case), closeness to speech can reasonably be a factor in the choice between them.
Jan
5
asked Has anyone read/debunked Yessenin-Volpin–Hennix “Beware of the Gödel-Wette paradox”?
Jan
5
comment How to refer to plural of mathematical symbols - with or without an apostrophe
In speaking, many mathematicians would pluralise it. Why not in writing also? Both options suggested are visually awkward, true; but it’s also awkward, in a different way, when orthography fails to follow speech.
Dec
25
comment Gluings and collages along profunctors
I would consider this just as the category of elements of $\varphi$, unless I’m missing something. How you would you see this as differing from any other construction of the category of elements?