Showing changes from revision #12 to #13:
Added | Removed | Changed
Contents
Definition in cohesive homotopy type theory
In real numbers
Let be the (two-sided) Dedekind real numbers with a term
representing that the shape of is contractible. and let be a closed interval or open interval in . Because the shape of is contractible, the shape of any closed or open interval in is contractible. Given a function mapping, let us define the graph of the function mapping as
in the product type . is continuous if the shape of is contractible:
Between geometrically contractible types spaces
Let and be types with termsspace?s with terms
representing that the shapes of and are contractible . Given a function mapping, let us define the graph of the function mapping as
in the product type . is continuous if the shape of is contractible:
Definition in homotopy type theory
In rational numbers
Let be the rational numbers. An function is continuous at a point
is pointwise continuous in if it is continuous at all points :
is uniformly continuous in if
In Archimedean ordered fields
Let be an Archimedean ordered field. An function is continuous at a point
is pointwise continuous in if it is continuous at all points :
is uniformly continuous in if
Most general definition
Let be a type with a predicate between the type of all nets in
and itself, and let be a type with a predicate between the type of all nets in
and itself.
A function is continuous at a point
is pointwise continuous if it is continuous at all points :
See also