3,490 reputation
1331
bio website peterlefanulumsdaine.com
location Stockholm, Sweden
age 32
visits member for 5 years
seen Dec 26 at 11:38

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