[[!redirects Sandbox > history]] [[!redirects Sandbox]] < [[nlab:Sandbox]] Dependent type theory is first and foremost a logic with equality. It differs from first-order logic with equality, but it is still a logic with equality. And indeed one could implement higher-order logic as a dependent type theory. One could also implement different kinds of mathematical foundations such as set theory, topos theory, and univalent type theory by postulating different kinds of universes via axioms and axiom schemata to work in. But that is irrelevant to the primary purpose of dependent type theory as a logic with equality. I am a pluralist and an agnostic when it comes to which foundations of mathematics to use. I don't really care how people view sets and the collection of all sets. However, I am monist when it comes to which ambient logic to use. category: redirected to nlab