Category Archives: Philosophy

It’s official: the author of MWA is not a philosopher

For anyone who read MWA it’s obvious that its author would never be mistaken for, nor would want to be mistaken for, a philosopher.  Still, three referees for the journal Synthèse were kind enough to put to rest any lingering doubts on that score (there were none) in their reviews of the article I have just posted on arXiv under the title Virtues of Priority.

In the fall of 2018 I received a message inviting me to contribute to “a special issue of the philosophy journal Synthèse on virtues and mathematics.”  The prospective guest editors wrote, “We would be delighted to be able to list you as a prospective contributor. This would, of course, be in no way binding on either party.”  This looked like the perfect excuse to write on a topic that had been much on my mind ever since the controversy broke out among number theorists on the correct attribution of the conjecture on modularity of elliptic curves.  From the very beginning this controversy was marked by the contrast between the acrimony with which certain colleagues addressed one another and the superficiality of the analysis with which they justified their positions.  Even while Wiles labored in secret in his attic, I was already wishing for a philosophical umpire to require the warring parties to base their arguments on general principles rather than on raw chronology and personal affinities.

The story is interesting, well written and the conjecture as well as the main actors play important roles in 20th century mathematics. In that sense the paper was a good read, but a good read is not enough to make a good philosophical paper.… The paper does not connect to the current debates on value ethics in mathematics at all; in fact, none of the papers on the reference list belongs to the philosophy of mathematics, and the most recent reference is from 2001. The paper should be situated more firmly in the recent literature on mathematical values … Along the same line, the paper does not make a clear and substantial contribution to current philosophical debates on virtues in mathematics. The paper does not contain a clear problem statement, and the virtues encountered in the historical case are only commented on en passant, but the paper does not provide a structured discussion or a collected conclusion. … The paper lacks methodological reflections. Why is the case in question a good case to explore the philosophical questions at hand and why are the chosen sources the right sources to explore the case? It should be made crystal clear why a dispute over priority of a conjecture is a good case to explore the nature of mathematical values.

A second referee was more encouraging:

This submission represents an excellent idea for an article and a solid initial effort at fulfilling that idea, not yet suitable for publication in Synthese.

but this indulgence can be dismissed because the referee is someone I know.  And, as this referee accurately perceived,

the virtue ethics aspect currently reads as something tacked on to a stimulating but not philosophy-journal-ready fireside/blackboard-side chat about a curious and gossip-ready extract of the history of the theory of elliptic curves.

The third referee’s objections came under three headings:  “The philosophical upshot of the paper is thin,” “The paper neglects other work on priority disputes,” and most tellingly, “The search for a functional significance of the dispute may be overstated”:

Merton observes that, in some instances, battles over priority have no functional significance (i.e., the authors fight over the priority of a finding even if the discoveries are independent and epistemically equivalent). This is due in part to the reward system of science. Moreover, along the same lines, there is a psychological explanation in terms of ego-protective biases. The paper should examine this possibility more closely.

This last objection is silly.  Referee number 3 may never have met anyone as ego-protective as several of the protagonists of the controversy, but the point of my essay was to ask whether the controversy might not shed some light on the value system driving contemporary mathematics — and “functional significance” is not the point either.

In nearly all other respects all three referees were absolutely right about the article.  It did not connect to current philosophical debates, it did not engage in methodological reflections, it neglects the literature on priority disputes, and it was not written in the style of a philosophical paper.  But this is not what I thought the editors had in mind when they asked a mathematician for a contribution.

I accepted the invitation to contribute to the special issue in good faith, on the assumption that the issue’s editors had good reason to believe that the thoughts of a professional mathematician on the roots of an unusually bitter controversy in the field would have a place in the journal, and could provide useful raw material for analysis by philosophers who are curious about the value systems that actually guide the practice of professional mathematicians, even though the mathematician in question has never claimed to be a philosopher.    Had the editors of this special issue made it clear to me that my submission would be judged on the basis of familiarity with “the current debates on value ethics in mathematics,” as these are pursued by philosophers who “have been taught mathematics at university level,” or by its author’s efforts to situate the submission in relation to “relevant secondary scholarship,” I would have replied that I have neither the time nor the inclination to undertake a project on that basis.  That the editors of Synthèse and the referees find it helpful to erect artificial barriers* to dialogue between professional scientists and those philosophers who claim to be interested in the values of such scientists is not my concern.   But I consider it unprofessional as well as irresponsible on the part of the issue’s editors to have failed at any time to explain to me the unfamiliar standards that would be applied to my article.

This was my response to the rejection letter from Synthèse, which concluded:

I would like to thank you very much for forwarding your manuscript to us for consideration and wish you every success in finding an alternative place of publication.

Finding a place of publication on arXiv was easy and is a perfectly satisfactory alternative, but philosophers may not think to look there for raw material.  I consulted with the philosopher David Corfield — who first convinced me of the relevance of Alasdair MacIntyre’s virtue ethics to mathematical practice in the article he published in Circles Disturbed — and he offered to help draw out the philosophical material through a dialogue on the n-Category Café.  His first comment on the arXiv publication is already online.

*In view of the events of the last few weeks, I am now ready to acknowledge that fears of disciplinary cross-contamination may be justified in some circumstances.

Reuben Hersh, 1927-2020 (with text)

Here is the introduction to my article Do Mathematicians Have Responsibilities, published in Humanizing mathematics and its philosophy.Essays celebrating the 90th birthday of Reuben Hersh.Edited by Bharath Sriraman. Birkhäuser/Springer, Cham (2017) 115-123.

I have been an admirer of Reuben Hersh ever since I received a copy of The Mathematical Experience, then brand new, as a birthday present.  At that stage, of course, I was admiring the tandem Reuben formed then, and on other occasions, with his co-author Philip J. Davis.  It was only almost 20 years later, after I started reading What is Mathematics, Really? that I could focus my admiration on Reuben — and not only on the mathematician, the author, the thinker about mathematics, but on the person Reuben Hersh — the unmistakable and unforgettable voice that accompanies the reader from the beginning to the end of the book.  So unforgettable was the voice, in fact, that when Reuben, wrote to me out of the blue three years ago to ask me what I thought about a certain French philosopher, I so clearly heard the voice of the narrator of What is Mathematics, Really? (and no doubt of many of the passages of his books with Davis) that I could honestly write back that I felt like I had known him for decades, though we have never met and until that time we had never exchanged a single word.

The voice in question is the voice of an author who is struggling to put words on an intense and intensely felt experience, who has intimate knowledge of how it feels to be a mathematician and also a knowledge no less intimate of the inadequacy of the language of our philosophical tradition to do justice to that experience, so that all attempts to do so inevitably end in failure; but this knowledge is compensated by the conviction that the stakes are so important that we can’t choose not to try.   What makes Reuben’s authorial voice compelling is that it sounds just as we expect the voice of a person in the middle of that struggle must sound.[1]   It’s the strength of this conviction that comes across in Reuben’s writing, so that reading his books and essays is remembered (by me, at least) as a conversation, a very lively conversation, filled with the passionate sense that we are talking about something that matters.  Also filled with disagreements — because I don’t always agree with everything I read in Reuben’s books and essays; beyond questions of detail the difference might come down to my sense that Reuben is trying to get to the bottom of the mathematical experience, whereas I apprehend the experience as bottomless; or I might say that it’s the effort to get to its bottom that is at the bottom of the experience.  But the differences are of little moment; what stays with me after reading a few pages of Reuben’s writing is the wholeness of the human being reflected in his words, a human being who cares so deeply about his mathematical calling that he is ready to add his own heroic failure to the long list of admirable failures by the most eminent philosophers of the western tradition to account for mathematics; and without these inevitable failures we would not begin to understand why it does matter to us.

[1] As I wrote that sentence I remembered that I have still not met Reuben, nor have I ever spoken to him; but I checked one of the videos online in which he appears and, sure enough, his literal voice is very much as I expected.

The soul of a space

The paper Česnavičius and Scholze just posted on arXiv answers several longstanding open questions in fundamental algebraic geometry.  It also introduces a new definition with energetic new terminology:


I don’t pretend to know which of the authors had the idea of returning to Latin roots in order to find the appropriate word to designate the objects that Lurie had chosen to call “spaces,” as well as their cognates in other settings.  Scholze’s terminological innovations have been more than commonly successful up to now, but I predict that “animated sets” will be especially popular.  A whole thesis in philosophy of mathematics — and a second thesis in theology of mathematics? — could be devoted to the last sentence above.

It turns out that the expression “soul of a space” has been popular for some time among interior designers and architects.


A room designed by architect Vipin Bakliwala

Bakliwala’s reply also deserves our attention:

As architects, it is our duty to induce emotions into a space and create an ambience that brings forth our hidden calm, positive and spiritual side. We strive to expand the brief given by the client and create a space that elevates and improves his life. We struggle to provide an environment which is an enhanced reflection of his thoughts. We call such places soul shelters.  It is that space where the soul remains in its innate nature.

Do emotions inhere more spontaneously in “worldly” point-set “physical” topological spaces or in their animated “calm, positive, and spiritual” ghostly doubles?  Descartes and Spinoza might help us sort this out.


UPDATE:  T.G. pointed out that, if I had read past the introduction to the acknowledgments, I would have realized that

The terminology is due to Clausen, inspired by Beilinson; see the acknowledgements, and the first paragraph of section 5.1.

Here is a passage from Beilinson’s article Topological E-factors that sheds some light on his perception of the need for appropriate terminology, and about the desolation of ordinary category theory.


A. A. Beilinson, Topological E-factors, Pure and Applied Mathematics Quarterly 3, 357-391, (2007)

Beilinson, or my imagined recollection of him, expresses a rather different opinion of spaces on p. 202 of MWA.

Roundtable video, incorrect proofs, true theorems

The Helix Center has now posted the video of Saturday’s round table on “Mechanization of Mathematics”.  The discussion was lively and everyone agreed that we should meet again, or even that we should organize a conference on the theme.

Since concern about correctness of proofs is one of the primary motivations of mathematicians who are active in automated proof verification, it was interesting to hear several colleagues at the IAS quote the following remark about Solomon Lefschetz:

He had marvelous intuition, and so far as I know, all of the results he claimed in algebraic geometry have now been proved. When I was a graduate student at Princeton, it was frequently said that “Lefschetz never stated a false theorem nor gave a correct proof.”

This is Philip Griffiths reminiscing, in his contribution to the biographical memoirs of Lefschetz (on p. 289).  The Helix Center discussion did raise the question of mechanizing mathematical intuition, but didn’t reach any conclusions.  The mathematicians I know would prefer to have correct proofs of correct theorems, but if our choice were between mechanical generators of false proofs of false theorems and false proofs of true theorems I guess we would pick the latter — especially if they were as consequential as the hard Lefschetz theorem.

And indeed, I was surprised to learn — but perhaps I should not have been — that Griffiths’s description of Lefschetz fits quite of few of the mathematicians I have most admired (I won’t name names).

Several people I admire were in the audience and others were watching the livestream.  Kevin Buzzard congratulated me for finding a way to quote William Burroughs (at 53′).  I repeat the quotation for the reader’s convenience:

[The] junk merchant does not sell his product to the consumer, he sells the consumer to his product. He does not improve and simplify his merchandise. He degrades and simplifies the client.

—William Burroughs, Naked Lunch

UPDATE:  A point I was trying to make at the roundtable, and also in the middle of this article, and in this post, about the inevitability of mechanization of mathematics (and of everything else, and of the monetization of the resulting data by tech companies), is made much more clearly and forcefully by Rose Eveleth in an article published today on Vox.


Roundtable on Mechanization of Mathematics

From the announcement:

Proof, in the form of step by step deduction, following the rules of logical reasoning, is the ultimate test of validity in mathematics. Some proofs, however, are so long or complex, or both, that they cannot be checked for errors by human experts. In response, a small but growing community of mathematicians, collaborating with computer scientists, have designed systems that allow proofs to be verified by machine. The success in certifying proofs of some prestigious theorems has led some mathematicians to propose a complete rethinking of the profession, requiring future proofs to be written in computer readable code. A few mathematicians have gone so far as to predict that artificial intelligence will replace humans in mathematical research, as in so many other activities.

One’s position on the possible future mechanization of proof is a function of one’s view of mathematics itself. Is it a means to an end that can be achieved as well, or better, by a competent machine as by a human being? If so, what is that end, and why are machines seen as more reliable than humans? Or is mathematics rather an end in itself, a human practice that is pursued for its intrinsic value? If so, what could that value be, and can it ever be shared with machines?

With Stephanie Dick, Brendan Fitelson, Thomas Hales, Michael Harris (who will largely follow the script already presented here), and Francesca Rossi.  At the Helix Center, 247 East 82nd St.

Mathematics, music, philosophy, and Alain Badiou


Panel at IRCAM, June 7, 2019.  Left to right:  François Nicolas, Yves André, Fernando Zalamea.  Alain Badiou is seated in the audience on the left.

To celebrate the publication of the third and final volume of Alain Badiou’s Being and Event trilogy, the organizers of the Paris MAMUPHI seminar — MAthématiques, MUsique, PHIlosophie — devoted a two-day conference at IRCAM (Institut de Recherche et Coordination Acoustique/Musique), under the title L’hypothèse du contemporain.

For the 20th anniversary of the Mamuphi seminar (mathematics-music-philosophy), these encounters are dedicated to L’Immanence des vérités, the latest work by the philosopher Alain Badiou, and, more particularly, to his theory of “works-in-truth”. How are works distinguished from “waste” and, incidentally, “archives”? The final part of the work by Badiou formalizes a limitless alternative to the oppression of finality. These days in June gather together mathematicians, musicians, philosophers, and the author to formulate their own hypothesis in the shadow of their reading of the contemporary in the 21st century.

Yves André invited me as one of the mathematicians, and because of my deep respect for André’s writings about mathematics — and of course for his mathematical work — I was pleased to accept the invitation.

Badiou’s three-volume system is heavily based on set theory and much of the third volume is devoted to the theory of large cardinals, with chapters on ultrafilters, theorems of Scott, Jensen, and Kunen, 0#, and much more.  I have no idea what the upcoming Columbia graduate workshop will make of all this.  My own presentation had nothing to do with set theory; my aim was to explain why Badiou was wrong to hint in his book, in passing, that the mathematics of Andrew Wiles belonged with the “waste,” or at best the “archives.”  You can watch my talk or you can read it (preceded by a couple of pages explaining my misgivings about the theme of the conference).

I have to confess a less highbrow motivation, though.  Here is an excerpt from a review by Stanley Chang of Mathematics without Apologies that appeared in Society, dated June 25, 2018.

Other reviewers, both academics and nonacademics, have quite forcefully deprecated his use of ideas without context, the irrelevancy of various sections, an unreadably poor organization, and a purposely opaque stream-of-consciousness that prohibits understand [sic] rather than encourages it. One of my own friends, an anthropologist in academia, laughingly said that his treatment of Badiou is something that you would expect from a bad first-year philosophy essay from a bad student at a bad university.

Although Chang gave excellent reasons for his evident dislike of the book, he went out of his way to give it a fair reading, and I have no problem with his review.  But why did he make up this part about Badiou?  MWA contains no “treatment of Badiou.”  According to the index, Badiou’s name appears three times, and only in endnotes.  Two of the references are direct quotations, without anything that can be construed as a “treatment,” and the third quotes Juliet Flower MacCannell’s comments on a quotation by Badiou regarding Lacan’s theory of love, along with Vladimir Tasić’s gloss on the quotation and the comments.

In the Q&A following my talk in Paris I got a laugh from Badiou by suggesting that the mere mention of his name would provoke the laughter of many American philosophers, not to mention anthropologists.  But I don’t think that explains Chang’s sentence.  Maybe he was confusing Badiou with Bourdieu?  Or maybe the treatment in question was on this blog, for example here?

I would fault the editors of Society for allowing the publication of that last sentence, or any sentence, on any subject whatsoever, that quotes an anonymous anthropologist — laughing no less — for the sole purpose of taking a cheap shot.  But in fact I have no idea what the sentence is about.

Genetic determinism once more obnubilates French readers

After a French friend informed a few of his American colleagues that the center-right weekly magazine Le Point had printed a translation of Ted Hill’s article in Quillette, in which he alleges that an article of his had been censored by both the Mathematical Intelligencer and the New York Journal of Mathematics on political grounds, I decided I had no alternative to wasting half an hour familiarizing myself with a few of the details.  Having done so, I am just going to reproduce the message I sent to my French friend.

But first:  the French verb obnubiler is usually translated “to obsess,” which has nothing in common with the English cognate obnubilate, which means literally to cloud.  But in fact, French dictionaries interpret obnubiler quite differently:  someone is described as obnubilé whose judgment is clouded or impeded by an obsession.  The obsessive and repeated attempts to explain differences in power and status by genetic factors is a good example of obnubilation in this sense.

Now for my message:

I really don’t want to be wasting my time on this, but I’m afraid I’m going to have to.  Here is a description of Quillette:

and here is an article by Gowers analyzing the claims in Hill’s alleged study.
There is a second post, in which Gowers goes to extreme lengths to give Hill’s theses the benefit of the doubt, while remaining unconvinced.
I’m not going to comment on the editorial process at the Intelligencer or the New York Journal of Mathematics, which is a matter of very little interest.  What I see is just one more strained effort to disguise as scientific inquiry a thoroughly artificial and simplistic framing of a complex interaction of phenomena for which one has nothing resembling a coherent model, motivated solely by the demonstrate that the present distribution of power and resources has a natural basis.  All of this has dramatic political implications and the “libertarians” with whom Quillette identifies may belong to all kinds of tendencies — Dawkins used to be some kind of leftist, Pinker is a [censored!] liberal, Charles Murray is definitely right-wing — but the organized forces overlap significantly with the alt-right.
The problem with this sort of online debate is that it’s presented as intellectual censorship, while in fact it’s something else entirely.  Most of the liberals who are confused by this framing would never defend the right of creationists or climate change deniers — or holocaust deniers — to equal time, in the name of freedom of expression.  But there is a surprising openness to polemics disguised as scientific analysis when the aim is to prove that women are inferior at one thing or another.
To my mind, the best response to claims about hereditary differences in intelligence is still Gould’s The Mismeasure of Man, which illustrates the lengths to which defenders of inequality will go in attempting to prove their theses.  That was written nearly 40 years ago.  (You may remember that he mentioned that at one point IQ tests had been used as scientific proof that Jews were intellectually inferior to northern Europeans.)  Gould wrote a shorter but no less devastating review of The Bell Curve in 1994.
Unfortunately this particular vampire has not yet been nailed to its tomb once and for all.  Here is what I wrote about this in the middle of an article about the responsibility of mathematicians, for the celebration of Reuben Hersh’s 90th birthday.

I want to discuss an older story, one in which the mathematical sciences play at most a supporting role, but that I think illustrates well how philosophical confusion about the nature of mathematics can interfere with informed judgment. Here is a sentence that, syntactically at least, looks like a legitimate question to which scientific investigation can be applied:

Does mathematical talent have a genetic basis?

On the one hand the answer is obviously yes: bonobos and dolphins are undoubtedly clever but they are unable to use the binomial theorem. The question becomes problematic only when the attempt is made to measure genetic differences in mathematical talent. Then one is forced to recognize that it is not just one question innocently chosen from among all the questions that might be examined by available scientific means. It has to be seen against the background of persistent prejudices regarding the place of women and racially-defined groups in mathematics. I sympathize as much as anyone with the hope that study of the cognitive and neurological basis of mathematical activities can shed light on the meaning of mathematics — and in particular can reinforce our understanding of mathematics as a human practice — but given how little we know about the relation between mathematics and the brain, why is it urgent to establish differences between the mathematical behavior of male and female brains? The gap is so vast between whatever such studies measure and anything resembling an appreciation of the difficulties of coming to grips with the conceptual content of mathematics that what really needs to be explained is why any attention, whatsoever, is paid to these studies. Ingrained prejudice is the explanation that Occam’s razor would select. But I’ve heard it argued often enough, by people whose public behavior gives no reason to suspect them of prejudice, that it would be unscientific to refuse to examine the possibility that the highlighted question has an answer that might be politically awkward. It’s the numerical form of the data, I contend, and the statistical expertise brought to bear on its analysis, that provide the objectivity effect, the illusion that one’s experiment is actually measuring something objective (and that also conveniently forestalls what ought to be one’s first reaction: why has Science devoted such extensive resources to just this kind of question?) The superficially mathematical format of the output of the experiment is a poor substitute for thought. Maybe something is being measured, but we have only the faintest idea of what it might be.

More concisely:  if the question is not scientific, then the answer won’t be scientific either.  Or even more concisely:  garbage in, garbage out.
I added some emphasis that was not, I think, in the original article.  I just want to conclude with a particularly helpful paragraph from Gould’s review of The Bell Curve.
Like so many conservative ideologues who rail against the largely bogus ogre of suffocating political correctness, Herrnstein and Murray claim that they only want a hearing for unpopular views so that truth will out. And here, for once, I agree entirely. As a card–carrying First Amendment (near) absolutist, I applaud the publication of unpopular views that some people consider dangerous. I am delighted that The Bell Curve was written–so that its errors could be exposed, for Herrnstein and Murray are right to point out the difference between public and private agendas on race, and we must struggle to make an impact on the private agendas as well. But The Bell Curve is scarcely an academic treatise in social theory and population genetics. It is a manifesto of conservative ideology; the book’s inadequate and biased treatment of data display its primary purpose—advocacy.
I think, though, that Gould would not have been so delighted to see the publication of the theses of The Bell Curve in a journal that seeks to maintain editorial standards.

Guest post by Kevin Buzzard

Kevin Buzzard wrote to let me know that WordPress rejected his comment on an earlier post, presumably because it was too long.  I reproduce it verbatim below.  It deserves to be read closely, in its entirety.  I have some thoughts about it, and I will write about them at some point, but for now I just want to leave you with this question:  do you agree with the claim in the last line that mathematicians “will have to come to terms with” the distinction he identifies, and will the “terms” necessarily be those defined by computer scientists?

This comment will somehow sound ridiculous to mathematicians, but since learning about how to formalise mathematics in type theory my eyes have really been opened to how subtle the notion of equality is.

A few months ago I formalised the notion of a scheme in dependent type theory, and whilst this didn’t really teach me any algebraic geometry that I didn’t already know, it did teach me something about how sloppy mathematicians are. Mathematicians think of a presheaf on a topological space as a functor from the category of open sets of the space to somewhere else (sets, groups, whatever). I have a very clear model of this category in my head — the objects are open sets, and there’s at most one morphism between any two open sets, depending on whether or not one is a subset of the other (to fix ideas, let’s say there’s a morphism from U to V iff U is a subset of V, rather than the opposite category, so presheaves are contravariant functors). But actually when formalising this definition you find that mathematicians do not use this category, they use an equivalent category (whose definition I’ll explain in a second). When formalising maths on a computer, this is a big deal.

Of course mathematicians are very good *indeed* at identifying objects which are “the same to all intents and purposes, at least when it comes to what we are doing with them right now”, e.g. two groups which are canonically isomorphic or two categories which are equivalent, and conversely I would like to suggest that actually computer scientists are quite bad at doing this — they seem to me to be way behind in practice (I had terrific trouble applying a lemma about rings in an application where I “only” had rings which were canonically isomorphic to the rings in the lemma, because in the system I was using, Lean, the automation enabling me to do this sort of thing is not quite ready, although progress is being made quickly). My gut feeling is that this situation is because there are too many computer scientists and not enough mathematicians involved in the formalisation process, and that this will change. In fact one of the reasons for my current push to formalise the notion of a perfectoid space in dependent type theory (note: not homotopy type theory) is to get more mathematicians interested in this sort of thing.

But back to the equivalence. Here is the surprising thing I learnt. Let X be a topological space. The actual category mathematicians use when doing sheaf theory is this. An object is a string of symbols in whatever foundational system you’re using, which evaluates to an open set. For example, X is an open set, as is (X intersect X), as is the empty set, as is (X intersect (the empty set)). Mathematicians instantly regard things like X intersect X as equal to X, because….well…actually why are they equal? They’re equal because two sets are equal if and only if they have the same elements — this is an axiom of mathematics. But when formalising maths on a computer, keeping track of the axioms you’re using is exactly what you have to do (or more precisely, getting the computer to invoke the axioms automatically when you need them is what you have to do). So X equals X intersect X, because of a *theorem* (or in this case an axiom, which is a special case of a theorem if you like; most theorems use several axioms put together in clever ways, this is a bit of a degenerate case). Mathematicians are so used to the concept of sets behaving like the intuitive notion of “a collection of stuff” that it’s very easy to forget that X = X intersect X is *not true by definition in ZFC*, it is true by the very first axiom of ZFC, but this is still a theorem. The elements are the same by definition, but equality of the elements implying equality of the sets is a theorem.

So the computer scientist’s version of the category of open sets is something like this: objects are valid strings of characters which one can prove are equal to open subsets of X, and there’s a morphism between U and V if and only if there’s a proof that U is a subset of V. In particular, in the example above there’s a morphism from X to X intersect X, and also a morphism from X intersect X to X, because both inclusions are theorems of ZFC (let me stress again that whilst both theorems are trivial, neither one is “true by definition” — both theorems need axioms from the underlying theory, absurd though it may sound to stress it). This makes the objects isomorphic, but not equal. Equality is a subtle thing for them!

The conclusion of the above (which of course a mathematician would regard as a fuss about nothing) is that computer scientists don’t work with the mathematician’s “skeleton” category, they work with an equivalent category, and hence get a notion of a sheaf which is canonically isomorphic to, but not strictly speaking equal to (in this extremely anal sense), the mathematician’s notion.

And how did I notice this? Why do I even care? It was when trying to prove that the pushforward of a sheaf F via the identity map id : X -> X was isomorphic to the sheaf you started with. I needed to come up with an isomorphism to prove this, and my first attempt failed badly in the sense that it caused me a lot of work. In practice one needs a map from F(U) to F(id U), for U any open set, with id U the image of U under the identity map (which equals U, by a theorem, which uses an axiom, and hence which is not true by definition). My first attempt was this: “prove id U = U, deduce that F(id U) = F(U), and use the identity map”. I then had to prove that a bunch of diagrams commuted to prove that this was a morphism of sheaves, and it was a pain because I really wanted this to be a complete triviality (as it is to a mathematician). I ran this past Reid Barton and he instantly suggested that instead of using equality to map F(U) to F(id U), I use the restriction map instead, because id U is provably a subset of U so there’s a natural induced map. I was wrong to use equality! I had too quickly identified U and id U because I incorrectly thought they were equal by definition. They are actually equal because of a trivial theorem, but to a computer scientist they are equal, but not definitionally equal, subsets of X, and this makes all the difference. Switching to res, all the diagrams commuted immediately from basic properties of the restriction map and indeed the computer proved commutativity of the diagrams for me. I was stunned.

In dependent type theory, there is at most one map from U to V, depending on whether or not there is a proof that U is a subset of V — all proofs of this give the same map. In homotopy type theory, different proofs give different maps, and in this particular situation this is not what we want — we actually get the wrong category this way — so presumably the homotopy type theory people have to do something else. I am not yet convinced that homotopy type theory is the right way to do all of mathematics (it works great for some of it, for sure). I am now convinced that dependent type theory can do all “normal” mathematics (analysis, algebra, number theory, geometry, topology) so I’m sticking here, but what I have learnt in the last year is that computer scientists seem to have several (competing!) notions of equality, and it is a subtlety which mathematicians are conditioned to ignore from an early age and which they will have to come to terms with one day.