bio | website | peterlefanulumsdaine.com |
---|---|---|
location | Stockholm, Sweden | |
age | 32 | |
visits | member for | 5 years |
seen | Dec 26 at 11:38 | |
stats | profile views | 2,742 |
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.
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? |
Dec 6 |
comment |
Is the defining bijection for a pullback of topological spaces a homeomorphism?
@AndrejBauer: in your last-but-one comment, should the domain of the step function be $(-\infty,0) \cup [0,\infty)$, i.e. with one of the intervals open at 0? |
Dec 4 |
comment |
Is the defining bijection for a pullback of topological spaces a homeomorphism?
@Andrej: my guess is that many people think of "constructive => continuous" just as a heuristic, and don't know there are formal statements; so your un-elaborated answer looked (to the downvoter) like invoking a heuristic as a proof. |
Dec 3 |
comment |
Small objects vs Compact objects
This shows what goes wrong if you try to prove that they are equivalent. But it would still be good to see a specific counterexample, as the question asks for! |
Dec 3 |
awarded | Yearling |
Nov 4 |
reviewed | Approve Is there some Riemannian manifold's version of Whitney theorem? |
Oct 25 |
comment |
A problem on chains of squares — can one find an easy combinatorial proof?
“I can show that there is no simple algorithm for your problem” — the complexity argument shows there can be no quick algorithm for the problem, but it doesn’t show there can’t be a simple one. Many problems have naïve exponential-time algorithms, which aren’t good for practical computation but can be great for understanding existence proofs easily. |
Oct 12 |
comment |
Concise definition of subobjects
I think the well-poweredness is beside the point: the main thing is that the groupoid core of the the category of subobjects is essentially discrete, and so we are quotienting by unique isomorphisms, which is generally well-behaved. |
Oct 2 |
comment |
What is the Complete Set of Shortest Axioms of Classical Conditional-Negation Propositional Calculus?
In infix notation, perhaps slightly more readable than prefix: [(((p→q)→(¬r→¬s))→r)→t] → [(t→p)→(s→p)]. |
Sep 29 |
comment |
What is the most useful non-existing object of your field?
This function exists; it just isn’t computable. A program computing this function could arguably be an answer. |
Sep 29 |
comment |
What is the most useful non-existing object of your field?
One can also argue that this one does exist, perfectly happily: it’s just a class that isn’t a set. |
Sep 23 |
revised |
Discrete Morse theory and existence of minimal complex
retagged (now that DMT tag exists) |
Sep 16 |
revised |
discrete-morse-theory wiki description
initiated wiki entry for new tag |
Sep 16 |
revised |
discrete-morse-theory wiki excerpt
initiated wiki entry for new tag |
Sep 16 |
revised |
Morse matching with 0-cells and (n-1)-cells
retagged (now that this tag exists) |
Sep 16 |
revised |
Discrete Morse theory and chess
retagged (now that tag exists) |
Sep 16 |
suggested | approved edit on discrete-morse-theory tag wiki |
Sep 16 |
wiki | created discrete-morse-theory description |
Sep 16 |
wiki | created discrete-morse-theory excerpt |
Sep 16 |
suggested | approved edit on discrete-morse-theory tag wiki excerpt |