Better scaffolding leads to bigger, better buildings. Don't knock the auxiliary and ancillary techniques; they're still necessary for this sort of work to be un

Better scaffolding leads to bigger, better buildings. Don't knock the auxiliary and ancillary techniques; they're still necessary for this sort of work to be understandable. Also, from my perspective, the exact real arithmetic isn't super-interesting because it's not new; Turing was doing this sort of thing when he first got access to computers. Legend has that one of Turing's first recreational programs was computation of zeros of the Riemann zeta function, and ever since, there's been a tradition of exploring exact real arithmetic with computers and programming languages. MarshallB is one more incremental step forward in a big research programme of overcoming the inconvenient fact that we can't test real numbers for interesting properties with computers alone. At no point have I advocated only category theory. Categories are always composed of some collection of arrows (and objects, but I prefer object-free presentations!), and those arrows are always homogeneous, if not homoousios, composed of a single substance. We can study that substance on its own. Perhaps an analogy to materials science would be appropriate. We ought to study both each building material, be it sets, vector spaces, relations, graphs, or type theories; but also the architectural principles used to make buildings, like abstract algebra and category theory.