# Homotopy Type Theory computable real numbers > history (Rev #1)

## 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))$