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. * [[an axiomatization of the real numbers]] ## Discrete mathematics * [[booleans]] * [[decidable universal quantifier]] * [[decidable existential quantifier]] * [[decidable directed graph]] * [[decidable setoid]] * [[decidable set]] * [[decidable preordered type]] * [[decidable strict order]] category: not redirected to nlab yet