Homotopy Type Theory Sandbox

The real numbers are a simplified model of numbers. Actual computation in reality occurs in the rational numbers.

The real square root does not actually exist. Instead we have a partial function on the rationals which is only approximately a square root up to some rational tolerance ϵ\epsilon.

−ϵ<sqrt ϵ(x) 2−x<ϵ-\epsilon \lt \mathrm{sqrt}_\epsilon(x)^2 - x \lt \epsilon

The same goes for analytic functions like the exponential function and the sine and cosine function.