[[!redirects Sandbox > history]] [[!redirects Sandbox]] < [[nlab:Sandbox]] The real problem with dependent type theory is that it is completely unsuitable for classically predicative and strongly predicative mathematics. Without function types and/or dependent function types, how does one define propositions, sets, equivalences, et cetera, and how does one express the recursion or induction principle of natural numbers? With function types, if one assumes excluded middle, then one is automatically working impredicatively, because power sets are function types into the booleans. category: redirected to nlab