bio | website | peterlefanulumsdaine.com |
---|---|---|
location | Stockholm, Sweden | |
age | 32 | |
visits | member for | 5 years, 9 months |
seen | 15 hours ago | |
stats | profile views | 3,055 |
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.
Aug
10 |
comment |
Grothendieck - sheaves as meter sticks
What was the original French wording, does anyone know? Some subtlety or alternative meaning might have been lost in translation. |
Aug
7 |
comment |
Mathematical software wish list
Tex was and is an extraordinary achievement, and is fantastic for what it is, and almost certainly superior to the alternatives, but (like any long-lived project) it has acquired a huge accumulation of cruft, much of which is rather dated. So if a dedicated team led by a clone of Knuth could write a new system, from the ground up, following the same principles as TeX and learning from what TeX’s many contributors have done in the mean time — I suspect we could end up with a significantly better system still. But there’s probably too much intertia for this to happen any time soon. |
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. |