3,569 reputation
1333
bio website peterlefanulumsdaine.com
location Stockholm, Sweden
age 32
visits member for 5 years, 7 months
seen 11 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.


May
18
awarded  Nice Question
May
13
comment Differential operators are coKleisli morphisms of the jet co-monad
I would expect this might appear in the synthetic differential geometry literature?
Apr
13
comment Does the Brouwer fixed point theorem admit a constructive proof?
It's difficult to assign a single rigorous meaning to it, because things that classically would all be considered as the BFPT (eg "BFPT for Cauchy reals" and "BFPT for Dedekind reals") may not be constructively equivalent. But once a single statement (up to constructive equivalence) is chosen, then certainly its constructive probability is a rigorous question.
Apr
6
comment Three-halves-free words (analogous to square-free)
@echinodermata: ah, thanks: I was considering extending it at the right-hand end not the left-hand end!
Apr
6
comment Three-halves-free words (analogous to square-free)
@echinodermata: Surely that word remains sandwich-free if extended by z? Is there a typo, or am I missing something?
Apr
6
comment Three-halves-free words (analogous to square-free)
I also played around a little with some code (in Haskell), and came to a similar conclusion. Indeed, I didn’t even manage to find a non-extendable sandwich-free word, i.e. a sandwich-free word with no sandwich-free extension, though my search was not exhaustive even for small lengths. Did you find any such?
Apr
5
comment Three-halves-free words (analogous to square-free)
@joro: no; since that permutation has order 3, the result will just repeat the 9-letter block (a,b,c,c,a,b,b,c,a) forever, so at 27 letters, if not before, it will contain a forbidden XYX (with Y=X).
Apr
5
comment Three-halves-free words (analogous to square-free)
“If a word has a square, it has a three-halves pattern” — really? Aren’t AA, or less trivially AABC and ABCABC, counterexamples? Or am I misunderstanding something?
Apr
2
comment Should one post a paper on the arXiv if it is not intended to be published?
@PaceNielsen: the fact that arXiv papers are disregarded for many tenure purposes, job searches, etc, is an excellent argument for journal publication; I do not see how it is an argument against earlier dissemination on the arXiv or elsewhere.
Apr
2
comment Historical (personal) examples of teaching-based research
This answer seems to have missed what the question was asking for.
Apr
2
revised Historical (personal) examples of teaching-based research
fixed typo
Apr
2
comment Historical (personal) examples of teaching-based research
@AlexandreEremenko: why do you dismiss that book as outrageous? There’s certainly much to disagree with in it — but in philosophy, much more than in maths, something can still be interesting, insightful, and worthwhile, even if one thinks it is fundamentally not true.
Apr
1
revised Applications of set theory in physics
edited reference to be readable without click-through
Apr
1
comment What should one “do” to “strictify” a triangle of transformations coming from a lax commutative triangle of functors?
@TimCampion: oops, that was a typo; I meant $\dashv$ throughout. Mikhail: once again, PLEASE can you clarify precisely what you are referring to as the “adjunction transformation”? It’s not standard terminology, and without knowing that, it’s very hard to answer your question.
Mar
31
comment What should one “do” to “strictify” a triangle of transformations coming from a lax commutative triangle of functors?
I don’t know, because I still don’t know what you mean by “adjunction transformation”! I’m guessing that you mean or the natural isomorphism $\mathbb{C}(fx,y) \cong \mathbb{D}(x,gy)$ (often called transposition). If you mean this, or the unit/counit, then they are determined up to strict equality; i.e. if $f \vdash g$ is an adjunction, with unit $\eta$ (or counit $\epsilon$, or transposition $\varphi$), and $g'$ is another functor with $\alpha:g'\cong g$, then there are unique $\eta'$ ($\epsilon'$, $\varphi'$) making $g'$ an adjoint to $f$, and commuting with $\alpha$.
Mar
31
comment What should one “do” to “strictify” a triangle of transformations coming from a lax commutative triangle of functors?
What do you mean by “adjunction transformations”? I’m not familiar with that terminology (and neither is Google, apparently).
Mar
26
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.