# Homotopy Type Theory continuous mapping > history (changes)

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

## Definition

### In real numbers

Let $\mathbb{R}$ be the Dedekind real numbers with a term

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

representing that the shape of $\mathbb{R}$ is contractible (which derives from axiom R-flat), and let $I$ be a closed interval or open interval in $\mathbb{R}$. Because the shape of $\mathbb{R}$ is contractible, the shape of any closed or open interval in $\mathbb{R}$ is contractible. Given a mapping $f:I \to \mathbb{R}$, let us define the graph $G$ of the mapping $f$ as

$G \coloneqq \sum_{x:I} (x, f(x))$

in the product type $I \times \mathbb{R}$. $f$ is continuous if the shape of $G$ is contractible:

$p:isContr(\esh(G))$

### Between geometrically contractible spaces

Let $S$ and $T$ be spaces with terms

$p_S:isContr(\esh(S))$
$p_T:isContr(\esh(T))$

representing that the shapes of $S$ and $T$ are contractible. Given a mapping $f:S \to T$, let us define the graph $G$ of the mapping $f$ as

$G \coloneqq \sum_{x:S} (x, f(x))$

in the product type $I \times \mathbb{R}$. $f$ is continuous if the shape of $G$ is contractible:

$p:isContr(\esh(G))$

## See also

Last revised on June 14, 2022 at 14:01:06. See the history of this page for a list of all contributions to it.