[[!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. ---- The important thing about impredicative types, such as function types, dependent function types, or the type of all propositions, is not that they satisfy universal properties, but rather that they allow non-element things, such as families of elements or types with at most one element, to be represented as elements of types. Are universal properties overrated? Only needed for the natural numbers... category: redirected to nlab