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. ## 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) ## Articles ported to the nLab ## * [[decimal numbers]] * [[rational numbers]] * [[irrational numbers]] * [[real numbers]] * [[directed type]] (directed set at nLab) * [[net]] and [[sequence]] * [[preconvergence space]] * [[limit of a net]] * [[Hausdorff space]] * [[sequentially Hausdorff space]] * [[premetric space]] * [[Cauchy net]] * [[modulus of Cauchy convergence]] * [[Cauchy approximation]] * [[Cauchy structure]] * [[HoTT book real numbers]] * [[generalized Cauchy real numbers]] * [[Cauchy real numbers]] * [[Cauchy real numbers (disambiguation)]] * [[quotient set]] * [[setoid]] * [[pre-algebra real numbers]] * [[Eudoxus real numbers]] * [[closed interval]] * [[lower bounded open interval]] * [[upper bounded open interval]] * [[open interval]] * [[unit interval]] * [[dyadic interval coalgebra]] * [[rational interval coalgebra]] * [[decimal interval coalgebra]] * [[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) * [[valuation (measure theory)]] * [[probability valuation]] * [[sigma-continuous valuation]] * [[sigma-continuous probability valuation]] * [[measure]] * [[probability measure]] * [[category of partial functions in a set]] * [[monoidal dagger category]] * [[braided monoidal dagger category]] * [[symmetric monoidal dagger category]] * [[cartesian monoidal dagger category]] * [[cocartesian monoidal dagger category]] * [[semiadditive dagger category]] * [[finitely complete dagger category]] * [[finitely cocomplete dagger category]] * [[compact closed dagger category]] * [[dagger 2-poset]] * [[onto dagger morphism in a dagger 2-poset]] * [[functional dagger morphism in a dagger 2-poset]] * [[entire dagger morphism in a dagger 2-poset]] * [[injective dagger morphism in a dagger 2-poset]] * [[map in a dagger 2-poset]] * [[monic map in a dagger 2-poset]] * [[epic map in a dagger 2-poset]] * [[category of maps]] * [[semiadditive dagger 2-poset]] * [[unital dagger 2-poset]] * [[tabular dagger 2-poset]] * [[division dagger 2-poset]] * [[power dagger 2-poset]] * [[elementarily topical dagger 2-poset]] * [[W-topical dagger 2-poset]] * [[well-pointed dagger 2-poset]] * [[coherent dagger 2-poset]] * [[geometric dagger 2-poset]] * [[Heyting dagger 2-poset]] * [[Boolean dagger 2-poset]] * [[Boolean topical dagger 2-poset]] * [[groupoid]] * [[ETCR]] * [[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]] * [[iterated differentiable function]] * [[smooth function]] * [[antiderivative]] * [[partial derivative]] * [[directionally differentiable function]] * [[directional derivative]] * [[sequence]] * [[sequential derivative]] * [[sequential antiderivative]] * [[left shift operator]] * [[right shift operator]] * [[series operator]] * [[inverse series operator]]