The other day my friend Lucas Salim was asking me some questions about categorical logic and constructive math, and he mentioned he’d never seen a proof that there’s no constructive proof of the intermediate value theorem before. I showed him the usual counterexample, and since my recent blog post about choice was so quick to write I decided to quickly write up a post about this too, since I remember being confused by it back when I was first learning it. The key fact is Soundness and Com...
