nLab set theory versus dependent type theory




The basis of it all

 Set theory

set theory

Foundational axioms

foundational axiom

Removing axioms



There are a few major differences between set theory and dependent type theory.


Set theory of all flavors, including material set theory and structural set theory, have two notions of logic,

Dependent type theory only has one notion of logic, which would correspond to the internal logic of the set theory. Thus, propositions are subsingletons.


Set theory of all flavors have only one notion of equality, propositional equality, which is a proposition in the external logic.

Most dependent type theories, like Martin-Löf type theory, cubical type theory, (higher) observational type theory, two-level type theory, simplicial type theory, et cetera, all have two notions of equality, judgmental equality and typal equality.

The only dependent type theory which only has one notion of equality is objective type theory, and corresponds to typal equality.

In addition, the equality in all set theories are by definition propositions, while only in set-level type theories such as those with UIP, axiom K, or boundary separation have subsingleton-valued typal equality. More general dependent type theories have equalities which could be sets, or types representing infinity-groupoids.


Categorical\;set theory has two notions of functions, either as elements of function sets fB Af \in B^A or as a primitives f:ABf \colon A \to B in the set theory. One could compare functions for equality in either case.

On the other hand, dependent type theory has only one notion of function which could be compared for equality: an element of a function type f:ABf \colon A \to B. The corresponding primitive notion is the concept of family of elements x:Af(x):Bx \colon A \vdash f(x) \colon B, of which there is no corresponding notion of equality of a family of elements.

See also

Last revised on January 21, 2023 at 06:37:42. See the history of this page for a list of all contributions to it.