Homotopy Type Theory Analysis > history (Rev #7)

Here we collect articles about doing analysis in HoTT.

General

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

Scalar differential calculus

• calculus 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

Real analysis

• real numbers
• premetric space
• Cauchy net
• Cauchy approximation
• modulus of Cauchy convergence
• Cauchy structure
• Cauchy real numbers
• HoTT book real numbers
• frame
• locale?
• sigma-frame
• sigma-locale?
• Sierpinski space
• localic real numbers?
• sigma-localic real numbers?
• Dedekind cut
• Dedekind real numbers
• MacNeille real numbers?
• open interval
• closed interval
• unit interval
• real unit interval?
• Eudoxus real numbers
• posite?
• ideal?
• filter
• Cauchy filter? and Cauchy space?

Functional analysis

…

References

• HoTT Book