Homotopy Type Theory Analysis > history (Rev #31, changes)

Showing changes from revision #30 to #31: Added | Removed | Changed

Here we collect articles about doing analysis in HoTT.

Analysis is the study of convergence and limits of nets, sequences, filters, and functions. Real analysis is about the study of convergence and limits of nets, sequences sequences, filters, and functions in Archimedean ordered fields and sequentially Cauchy complete Archimedean ordered fields. (Dedekind complete Archimedean ordered fields do exist but I would rather move those to the list on topology because the definition is fundamentally topological rather than analytical.)

…what are the necessary requirements for the existence of an inverse: that the field be sequentially Cauchy complete, as the Banach fixed point theorem used to prove the inverse function theorem requires the metric to be sequentially Cauchy complete.

Cauchy sequences

• sequence
• sequential convergence space
• limit of a sequence
• sequentially Hausdorff space
• Cauchy sequence
• sequentially Cauchy complete Archimedean ordered field
• real numbers
• uniformly continuous function

Pointwise analysis

• limit of a function
• pointwise continuous function
• function limit space

Intervals

• open interval
• lower bounded open interval
• upper bounded open interval
• closed interval
• unit interval
• dyadic interval coalgebra
• rational interval coalgebra
• decimal interval coalgebra

Differential calculus

• function limit space
• limit of a function
• pointwise continuous function
• algebraic limit field
• limit of a binary function approaching a diagonal
• difference quotient
• differentiable function
• Newton-Leibniz operator
• derivative
• inverse image
• iterated inverse image
• infinitely iterated inverse image
• iterated differentiable function
• smooth function
• antiderivative
• algebraic limit vector space?
• partial derivative
• directionally differentiable function
• directional derivative
• algebraic limit Clifford algebra?
• algebraic limit geometric algebra?
• geometric derivative?

References

• HoTT Book