> This is one reason why type theory is superior to set theory. In type theory we can actually capture the abstract concept of real number and work with it, ins

> This is one reason why type theory is superior to set theory. In type theory we can actually capture the abstract concept of real number and work with it, instead of always working with an encoding. Could you give a small example of how a simple bit of reasoning about a real (or even natural) number would work in both frameworks?