Homotopy Type Theory Analysis > history (Rev #27)

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, filters, and functions in Archimedean ordered fields and sequentially Cauchy complete Archimedean ordered fields.

General

• directed type
• net and sequence
• filter of subsets?
• preconvergence space
• limit of a net
• Hausdorff space
• sequentially Hausdorff space

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
• calculus Clifford algebra?
• calculus geometric algebra?
• geometric derivative?
• uniformly continuous function

Cauchy spaces

• premetric space
• Cauchy net
• Cauchy approximation
• modulus of Cauchy convergence
• Cauchy structure
• modulated Cauchy real numbers
• HoTT book real numbers
• Cauchy complete Archimedean ordered field

Real analysis

• real numbers
• infinite decimal representation of a unit interval
• pre-algebra real numbers
• real unit interval?
• frame
• locale?
• Dedekind cut
• Dedekind real numbers
• Dedekind cut structure
• Dedekind cut structure real numbers
• interval cut
• Dedekind real closed intervals
• Dedekind complete Archimedean ordered field
• Dedekind complete Archimedean ordered integral domain
• sigma-frame
• sigma-locale?
• Sierpinski space
• localic real numbers?
• sigma-localic real numbers?
• MacNeille real numbers?
• Eudoxus real numbers
• posite?
• ideal?
• filter
• an axiomatization of the real numbers

Functional analysis

…

References

• HoTT Book