# Homotopy Type Theory contractibility of Dedekind real numbers > history (changes)

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

## Definition

Axiom: The

shape of $\mathbb{R}$ is contractible:

$p:isContr(\esh(\mathbb{R}))$

This statement can be derived from axiom R-flat