Showing changes from revision #11 to #12:
Added | Removed | Changed
Contents
Definition in cohesive homotopy type theory
Let and be types with terms
In real numbers
Let be the (two-sided) Dedekind real numbers with a term
representing that the shapes of and are contractible. A function is continuous if the shape of the curve defined by
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 , let us define the graph of the function as
in the product type is contractible:
in the product type . is continuous if the shape of is contractible:
Between geometrically contractible types
Let and be types with terms
representing that the shapes of and are contractible. Given a function , let us define the graph of the function 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