bio  website  peterlefanulumsdaine.com 

location  Stockholm, Sweden  
age  32  
visits  member for  5 years, 3 months 
seen  6 hours ago  
stats  profile views  2,878 
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 CalkinWilf. This representation obtains positive rationals using the operations $a$, “add one”, and $i$, “add one, then invert”; CalkinWilf 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 CalkinWilf 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 higherlevel 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 nonnegative 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 nonnegative rationals and binary sequences. On the other hand, the usual binary representation gives a bijection between binary sequences and nonnegative 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 downvoted: 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 ErdosTuran. 
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 closevote camp, though as “primarily opinionbased” rather than “offtopic”. 
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 wellanswered 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 ontopic here to me. 
Jan 5 
comment 
Has anyone read/debunked YesseninVolpin–Hennix “Beware of the GödelWette 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 explicitlypluralisedwitha[z]phoneme version is more common/natural than the zeropluralised 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 zeropluralised written form as representing the explicitlypluralised 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 YesseninVolpin–Hennix “Beware of the GödelWette 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? 