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 :isContr(esh())p_\mathbb{R}:isContr(\esh(\mathbb{R}))

representing that the shape of \mathbb{R} is contractible (which derives from axiom R-flat), and let II 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:If:I \to \mathbb{R}, let us define the graph GG of the mapping ff as

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

in the product type I×I \times \mathbb{R}. ff is continuous if the shape of GG is contractible:

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

Between geometrically contractible spaces

Let SS and TT be spaces with terms

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

representing that the shapes of SS and TT are contractible. Given a mapping f:STf:S \to T, let us define the graph GG of the mapping ff as

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

in the product type I×I \times \mathbb{R}. ff is continuous if the shape of GG is contractible:

p:isContr(esh(G))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.