Peter LeFanu Lumsdaine

less info
3,442 reputation
1231
bio website mathstat.dal.ca/…
location Halifax, Canada
age 31
visits member for 4 years, 7 months
seen yesterday

math.LO/math.CT, currently at the Institute for Advanced Study, Princeton, lately of Dalhousie University, Nova Scotia, and Carnegie Mellon University, Pittsburgh.


2d
comment Rediscovery of lost mathematics
@hobbs: it reminds me nicely of Lewis Carroll’s long but charming Phantasmagoria, which also uses a mixed pattern of 4-foot and 3-foot lines, in that case in 5-line stanzas (4 / 3 / 4 / 4 / 3).
Jul
2
awarded  Curious
Jun
30
comment What is semantics of “type”? Do “types” of “type theory” semantically differ from “set” of set theory?
@YemonChoi: thanks, fixed!
Jun
30
comment What is semantics of “type”? Do “types” of “type theory” semantically differ from “set” of set theory?
I think this question would be better-suited to math.stackexchange.com — it’s a fairly introductory question on the subject. If you re-ask it there, and ping me by replying to this comment, I’ll answer it there. Very roughly, though: the types of computer science correspond not so much to the type theories of Russell, Quine, etc., but more to the type theories of Curry, Church, etc — e.g. the simply-typed lambda-calculus — and there is lots of mathematical work on these systems and their semantics.
May
9
comment Does Grothendieck have any pseudonymous paper?
@quid: it is certainly sensationalist, but in what way is it vague? The criterion for answers seems quite clear: publicly available work that does not carry Grothendieck's name, but which there's some reason to believe that Grothendieck may have written.
May
2
comment Submitting a companion paper with detailed proofs ?
@TimothyChow: while I don't disagree with your points in general, the length restriction in JAMS seems to be no longer current --- looking at recent issues, most have at least one paper of $\geq$ 60pp, and there are even a few around the hundred-page mark.
Apr
29
answered Generalizing indexed coproduct from $\mathrm{Set}$ to other monoidal categories
Apr
29
comment Generalizing indexed coproduct from $\mathrm{Set}$ to other monoidal categories
@BrentYorgey: you say in the first comment that you don't want to use the "pick some ordering of J, then use this to take the J-iterated monoidal product" approach, because you're working in a constructive setting. However, what definition of "finite" are you using for J? In such settings there are several options for this‌​? If you assume that J is cardinal-finite, then you can use the indexed-monoidal-product approach without difficulty. In fact, I may expand this into an answer.
Apr
20
comment Have axioms / axiom schemata of this flavour been proposed or otherwise considered?
@user18921: I guess it’s that I find your classification rather un-compelling — particularly the suggestion that “more complicated sets from less” axioms tend to satisfy uniqueness properties, while “bigger from smaller” tend not to.
Apr
20
comment Have axioms / axiom schemata of this flavour been proposed or otherwise considered?
You set up uniqueness as part of the distinction, but in the examples you give of type (2) (Union and Powerset), the sets asserted are unique; and one of your examples for (1), Replacement, is often given in a equivalent form (Collection) which does not satisfy uniqueness.
Apr
19
comment For which Millennium Problems does undecidable -> true?
@ChristianRemling: “The truth of a conjecture can’t make a set $\Pi^0_1$ if it wasn't so to start with.” Sure, but the $\Pi^0_1$-ness of a set can be implied by (or even equivalent to) some conjecture. A proof of the conjecture can’t change whether the set is $\Pi^0_1$, but it can tell us whether or not it is.
Apr
7
revised Why is a braided left autonomous category also right autonomous?
expanded answer, attempted to fix latex, added disclaimer for unfixed parts.
Apr
7
answered Why is a braided left autonomous category also right autonomous?
Mar
28
revised On the Complement of a subgroup
fixed link (and grammar)
Mar
10
reviewed Approve suggested edit on self-dual representations
Mar
8
comment Intuitive crutches for higher dimensional thinking
@KConrad: your joke reminds me of a musical version I witnessed. Most musicians have at some point learned to play triplets against duplets — one of your hands plays 2 evenly spaced notes per beat, the other hand plays 3. 3-against-4 is also not uncommon, and in ≥C20th music, higher divisions also occur. At this particular dinner, one pianist marvelled that another could play a perfectly even 13-against-14 rhythm; a composer present was surprised at the surprise. “But it’s easy, isn’t it? You just set up one hand playing 13, and the other playing 14, and then you put them together!”
Mar
8
awarded  Notable Question
Feb
25
comment Historical quotation search: Equations/formulae in (Latin?) prose, before modern symbolic notation
@PietroMajer: that’s fascinating! Can you suggest any good sources for seeing the intermediate stages? Or, even better, any articles about this transition?
Feb
25
accepted Historical quotation search: Equations/formulae in (Latin?) prose, before modern symbolic notation
Feb
24
revised Historical quotation search: Equations/formulae in (Latin?) prose, before modern symbolic notation
added link to this question at the HoM Area 51 proposal