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.