Type theory is a foundational language for mathematics (i.e. an alternative to set theory). However, it behaves differently from set theory. For instance, a set-theoretic foundation has two layers: (1) a deduction system (e.g. first order logic), and (2) some axioms formulated inside this system (e.g. axioms of ZFC). Therefore, set theory is not only about sets, but rather about the interplay between sets (objects of the second layer) and propositions (objects of the first layer).
In constrast, type theory has its own deductive system. Instead of working with propositions and sets in set theory, type theory uses the notion of types and terms. Propositions are identified with particular types; and thus proving a theorem corresponds to the mathematical activity of constructing an term (called an inhabitant) of a type that represents the proposition.
A deductive system consists of a collection of judgments with rules to derive them. This is analogous to positions with rules in game theory, and elements with operations in an algebraic theory.
In type theory, the most basic judgment is " ", read as "the term has type ". When is a type representing a proposition, then may be regarded as an evidence to the truth of (or even a proof of ).
We sometimes can treat the type as a set, then " " can be interpreted as analogous to the set-theoretic statement " ". However, an essential difference is that " " is a judgment whereas " " is a proposition. In particular, we cannot "disprove" the judgment " " or make statements such as "if then it is not the case that " when working internally in a type theory.
One way to think about it is that the set-theoretic "membership" is a predicate that may or may not hold between two pre-existing sets and , but in type theory, we cannot talk abount an element is isolation. This is because every element is by nature an element of some type. For instance, when we say informally "let be a natural number", the set-theoretic interpretation is "let be a set and assume ", but in type theory "let " is an atomic statement: we cannot introduce a variable without specifying its type.
The last difference between type theory and set theory is the treatment of equality. In mathematics, the familiar notion of equality is a proposition: e.g. we can disprove an equality or assume it as a hypothesis. In type theory, this correspond to the equality type " " given . When is inhabited, we say that and are propositionally equal.
However, we also need a notion of equality as a judgment, denoted , or simply . For instance, if we define a function by , then is equal to by definition. A judgmental equality (or definitional equality) is then useful when we have derived the judgment for some , and wolud like to use it to derive an inhabitat for the type , since is by definition. Ultimately, we want a rule saying that given the judgments and , we can derive the judgment .