Homotopy Type Theory Discrete mathematics > history (Rev #30)

These articles should be ported to the nLab or merged into the existing article on the 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.

 Articles ported to the nLab

• decimal numbers
• rational numbers
• irrational numbers
• real numbers
• sequentially Hausdorff space
• quotient set
• setoid
• 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
• Dedekind cut (disambiguation) (mostly for the predicative Dedekind cuts)
• Dedekind real numbers (disambiguation) (mostly for the predicative Dedekind real numbers)
• groupoid
• 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
• bidirectional sequence