bio | website | peterlefanulumsdaine.com |
---|---|---|
location | Stockholm, Sweden | |
age | 32 | |
visits | member for | 5 years, 7 months |
seen | 11 hours ago | |
stats | profile views | 2,993 |
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. |