[[!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. ---- One also has to be a pluralist when it comes to equality, because there are at least 5 different notions of equality in dependent type theory ---- 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... ---- Just kind of accept that there are Martin-Löf higher order logic, cubical higher order logic, observational higher order logic, etc.... The difference is that Tarski types of all propositions is a rejection of the propositions as types and the propositions as some types philosophy. Propositions are only codes for subsingletons in higher order logic. category: redirected to nlab