> They are sequences, not sets. I get what you are trying to say here. If we were talking only about calculus, it would be a reasonable thing to say. In this c

> They are sequences, not sets. I get what you are trying to say here. If we were talking only about calculus, it would be a reasonable thing to say. In this context, we are talking about calculus in connection with its set theory foundations, and so this statement, in context, is simply incorrect. Imagine I dropped a tomato on the floor and called you in to help me clean up a “chemical spill”. You’d say that’s not a chemical spill, that’s a tomato. On any other day of the year you would be correct, but today we are in chemistry class, talking about how ordinary matter is made of chemicals. Today you are wrong, because we are in chemistry class, talking about what tomatoes are made of. > Putting types into a model of mathematics seems to add a very welcome firewall between algebraic structures (like the reals) and the underlying formalism that was used to justify their existence and properties. The firewall only works if the underlying structure is sound. People have, historically, spent enormous amounts of time working with mathematical objects that turned out to be trivial, turned out not to exist at all, or had contradictions. For that reason, real mathematicians spend some time fussing about proving that the real numbers exist using set theory, before they turn around and work with exactly that firewall that you’re discussing. In upper-level undergrad courses, you’ll be expected to do this. (At least, I was asked to do this in undergrad.) Again, today, the topic of discussion is the axiom of infinity. If I ask, “how would we do calculus without infinite sets,” we need to revisit the set-theoretic construction of real numbers and calculus before we can put that firewall back into place. > But I don’t have to worry about Banach-Tarski when integrating a function. Unfortunately, the Banach-Tarski paradox is exactly the kind of paradox you must worry about when integrating functions. In a loose sense, what the paradox shows is that you cannot cut up a function you want to integrate, rearrange the pieces, and then integrate the result. For a long time, mathematicians had all sorts of incorrect beliefs about calculus. For example, “a continuos function defined on an open interval is differentiable at some point on the interval”. These incorrect beliefs didn’t disappear overnight. We created a rigorous foundation for calculus on a carefully-crafted list of set theory axioms (ZFC) and slowly rooted out the incorrect beliefs with proofs and counterexamples. It’s worth asking whether ZFC is the foundation we want for calculus. Maybe it’s time to adjust the foundations. Maybe you think—what if I had a version of calculus that didn’t have non-measurable sets? Working backwards from that idea, what axioms would I need in order to still get work done?