It's not `noncomputable` in Lean though. Lots of computable functions use it.

I've read Bauer's paper before btw. I think topoi are cool, but I don't think it's a complexity worth thinking about for everyone else who isn't concerned about these things.