Homotopy Type Theory Analysis > history (Rev #1)

Here we collect articles about doing analysis in HoTT.

Real analysis

• real numbers
• directed type
• net and sequence
• Cauchy net
• limit of a net
• premetric space
• 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?
• eventuality filter? and convergence space?

Functional analysis

…

References

• HoTT Book