Homotopy Type Theory Sandbox (Rev #11)

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) 2x<ϵ-\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.

Revision on April 12, 2025 at 01:50:51 by Anonymous?. See the history of this page for a list of all contributions to it.