Homotopy Type Theory Analysis > history (Rev #23)

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

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