# Homotopy Type Theory computable real numbers > history (changes)

Showing changes from revision #1 to #2: Added | Removed | Changed

## Definition

A computable real number is an element of an

Archimedean ordered field $F$ with either

$\epsilon(c):\prod_{a:\mathbb{Q}} \prod_{b:\mathbb{Q}} (a,b) \to ((a,c) + (c,b))$