Homotopy Type Theory Analysis > history (Rev #4)

Here we collect articles about doing analysis in HoTT.

General

• directed type
• net and sequence
• limit of a net
• Hausdorff space
• limit of a function
• continuous 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