Homotopy Type Theory Analysis > history (Rev #24)

Here we collect articles about doing analysis in HoTT.

1. General

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

2. Pointwise analysis

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

3. Intervals

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

4. 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

5. 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

6. 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
• 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

7. Functional analysis

…

8. References

• HoTT Book