Homotopy Type Theory Sandbox (Rev #13, changes)

Showing changes from revision #12 to #13: Added | ~~Removed~~ | ~~Chan~~ged

~~The real numbers are a simplified model of numbers. Actual computation in reality occurs in the rational numbers.~~ $\Sigma \simeq \mathrm{bool}$ the initial $\sigma$ -frame, and the $\sigma$ -topological space being countably compact: every countable open cover has a finite subcover?

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

Revision on April 14, 2025 at 19:54:38 by Anonymous?. See the history of this page for a list of all contributions to it.