[[!redirects Sandbox > history]] [[!redirects Sandbox]] < [[nlab:Sandbox]] Dependent type theory as logic vs dependent type theory as foundations The former uses a separate type judgment, while the latter uses universe levels (Peano arithmetic or Heyting arithmetic) and Russell or Coquand universes. category: redirected to nlab