[[!redirects analysis]] [[!redirects Analysis in HoTT]] 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]]