These articles should be ported to the [[nLab:HomePage|nLab]] or merged into the existing article on the [[nLab:HomePage|nLab]] because although the concepts in many of the articles were originally developed in homotopy type theory, they are general enough that they should be of interest to classical and constructive mathematicians who do not use homotopy type theory as foundations. ## Numbers ## * [[decimal numbers]] * [[rational numbers]] * [[irrational numbers]] ## Cauchy real numbers ## * [[premetric space]] * [[Cauchy net]] * [[modulus of Cauchy convergence]] * [[Cauchy approximation]] * [[Cauchy structure]] * [[HoTT book real numbers]] * [[quotient set]] * [[Cauchy real numbers]] * [[generalized Cauchy real numbers]] * [[Cauchy real numbers (disambiguation)]] ## Dedekind real numbers ## * [[lattice]] * [[distributive lattice]] * [[sigma-complete lattice]] * [[sigma-frame]] * [[Sierpinski space]] * [[Dedekind cut (disambiguation)]] (mostly for the predicative Dedekind cuts) * [[Dedekind real numbers (disambiguation)]] (mostly for the predicative Dedekind real numbers) ## Other real numbers ## * [[real numbers]] * [[Eudoxus real numbers]] ## Measure theory ## * [[valuation (measure theory)]] * [[probability valuation]] * [[sigma-continuous valuation]] * [[sigma-continuous probability valuation]] * [[measure]] * [[probability measure]] ## Centipede analysis ## Centipede in the sense of centipede mathematics * [[directed type]] (directed set at nLab) * [[net]] and [[sequence]] * [[preconvergence space]] * [[limit of a net]] * [[limit of a function]] * [[continuous function]] (continuous map at nLab) * [[Hausdorff space]] * [[sequentially Hausdorff space]] ## Intervals ## * [[closed interval]] * [[open interval]] * [[unit interval]] ## Precategory theory ## * [[precategory]] * [[Rezk completion]] * [[category]] (probably should be univalent category at nLab) * [[dagger precategory]] * [[dagger category]] (probably should be univalent dagger category at nLab) ## Concrete categories ## * [[category of partial functions in a set]] * [[ETCR]]