nLab higher-level foundations

Definition

By higher-level foundations, or simply higher foundations, we mean any foundation of mathematics in which there are, or at least can be, basic objects of h-level higher than h-sets. Thus, these objects behave like groupoids or infinity-groupoids (or even categories or infinity-categories). This is in contrast to set-level foundations such as set theory and set-level type theory in which all objects behave like sets.

Some higher-level foundations include:

• homotopy type theory / univalent foundations of all sorts:
  • Book HoTT
  • cubical type theory, including CCHM cubical type theory, Cubical Agda, and Cartesian cubical type theory
  • higher observational type theory
• More generally, intensional type theory, in which no types of higher h-level can be shown to exist, but neither can all types be shown to be h-sets.
• formal category theory
• synthetic (infinity,1)-category theory, such as simplicial type theory and bicubical type theory
• Hypothetical elementary theories of the bicategory of categories and the (2,1)-category of groupoids, expressed in first-order logic with dependent sorts in the same way that ETCS is. One extant theory along these lines is ETCC, although it hasn’t been successfully made into a full foundation of mathematics.