Skip to main content
Search type Search syntax
Tags [tag]
Exact "words here"
Author user:1234
user:me (yours)
Score score:3 (3+)
score:0 (none)
Answers answers:3 (3+)
answers:0 (none)
isaccepted:yes
hasaccepted:no
inquestion:1234
Views views:250
Code code:"if (foo != bar)"
Sections title:apples
body:"apples oranges"
URL url:"*.example.com"
Saves in:saves
Status closed:yes
duplicate:no
migrated:no
wiki:no
Types is:question
is:answer
Exclude -[tag]
-apples
For more details on advanced search visit our help page
Results tagged with
Search options answers only not deleted user 2273

Questions that are about research in mathematics, or about the job of a research mathematician, without being mathematical problems or statements in the strictest sense. Do not use this tag for easy or supposedly easy mathematical questions.

2 votes

What do people mean by "subcategory"?

I think in practice, most people would (if pressed) describe the definition they're using as something like the Mac Lane definition, plus being allowed to replace either category with another equivale …
Peter LeFanu Lumsdaine's user avatar
17 votes

What is the endgoal of formalising mathematics?

Other answers address several aspects of your question, but to add a point not mentioned yet — you write: it seems to me that we are currently creating new mathematics at a far greater rate than we a …
6 votes

Theorem versus Proposition

Besides the points mentioned in other answers, a theorem or proposition is usually something whose main import is reasonably clear from the statement. A lemma, by contrast, is often a statement whose …
13 votes

Papers on arXiv solving the same problem at the same time

I was involved in one such pair: Van den Berg, Garner, Types are weak $\omega$-groupoids, https://arxiv.org/abs/0812.0298 Lumsdaine, Weak $\omega$-categories from intensional type theory, https://ar …
4 votes

Publishing corollaries of previously published results

To avoid salami-slicing, just keep the size and claims of the new paper appropriately modest. The problematic sense of salami-slicing is when a twenty-page paper appears to claim complete novelty, bu …
Peter LeFanu Lumsdaine's user avatar
11 votes

Role of univalence in homotopy group calculations

This is essentially the same content as earlier answers, but I’ll try to emphasise the aspect OP is asking about a bit more explicitly. $\newcommand{\Z}{\mathbb{Z}}$I’ll use the terminology of “paths …
Peter LeFanu Lumsdaine's user avatar
12 votes

Geometric intuition for limits

Since you're familiar with the example of the sheaf condition, I think a nice one-liner intuition is: A limit of a diagram is an object of matching families in that diagram. ...defined just like …
Peter LeFanu Lumsdaine's user avatar
49 votes

Why are matrices ubiquitous but hypermatrices rare?

An awfully simplistic answer: we work on two-dimensional paper, so two-dimensional matrices are very convenient to write down and compute with, while higher-dimensional hypermatrices are not. So whil …
Peter LeFanu Lumsdaine's user avatar
7 votes

Books containing new results

The Homotopy Type Theory book, from 2013 — ten years ago this summer — collaboratively written by many authors, myself included, and containing a lot of original work (some published as papers in para …
15 votes

Most intriguing mathematical epigraphs

Lévy [...] once remarked to me that reading other mathematicians’ research gave him actual physical pain. A quotation from J.L. Doob, on Paul Lévy, used as an epigraph by Tom Leinster in A survey …
2 votes

Technical term for representing object of a presheaf determined by a left-adjoint?

Todd Trimble’s answer makes very good points about representing objects/arrows in general. However, in your specific case — an object $c \in \newcommand{\C}{\mathbf{C}}\newcommand{\D}{\mathbf{D}}\C$ …
Peter LeFanu Lumsdaine's user avatar
17 votes
Accepted

Why are W-types called "W"?

You write: Probably "W" means either "wellordered" or "wellfounded". […] But these are notions associated to order theory, whereas W-types don't directly have to do with order relations (if at all). …
Peter LeFanu Lumsdaine's user avatar
5 votes

Book that shows a construction of ZFC with Calculus of Constructions

As noted by Reid Barton in comments, the Homotopy Type Theory book is probably the closest to what you ask for. It introduces its dependent type theory (which is essentially CIC plus extra assumption …
Peter LeFanu Lumsdaine's user avatar
13 votes
Accepted

Is the logic of the ($\infty$-?)topos of simplicial sets "contradictory up to homotopy"?

No, it’s not “inconsistent up to homotopy” — by combining the (strict) subobject classifier with the idea that contractible=trivial, you’re mixing two different logical languages for simplicial sets, …
Peter LeFanu Lumsdaine's user avatar