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$.

$$-\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.