types. The research into this property led to cubical type theory, where the property holds without needing an axiom. "Law of Excluded Middle" is often added to satisfy users who want classical logic, instead of intuitionistic logic. The Axiom of Choice does not need to be added to type theory, because in most type theories it can be derived from the rules of inference. This is because of the constructive nature of type theory, where proving that a value exists requires a method to compute the value. The Axiom of Choice is less powerful in type theory than most set theories, because type theory's functions must be computable and, being syntax-driven, the number of terms in a type must be countable. (See .) Decision problems A type theory is naturally associated with the decision problem of type inhabitation. Type inhabitation The decision problem of type inhabitation (abbreviated by ) is: Given a type environment and a type , decide whether there exists a term that can be assigned the type in the type environment . Girard's paradox shows that type inhabitation is strongly related to the consistency of a type system with Curry–Howard correspondence. To be sound, such a system must have uninhabited types. The opposition of terms and types can also be views as one of implementation and specification. By program synthesis (the computational counterpart of) type inhabitation (see below) can be used to construct (all or parts of) programs from specification given in form of type information. Type inference Many programs that work with type theory (e.g., interactive theorem provers) also do type inferencing. It lets them select the rules that the user intends, with fewer actions by the user. Research areas Homotopy type theory differs from intuitionistic type theory mostly by its handling of the equality type. In 2016 cubical type theory was proposed, which is a homotopy type theory with normalization. Interpretations Type theory has connections to other areas of mathematics. Proponents of type theory as a foundation often mention these connections as justification for its use. Types are propositions; terms are proofs When used as a foundation, certain types are interpreted as propositions (statements that can be proven) and a term of the type is a proof of that proposition. Thus, the type "Π x:nat . x+1=1+x" represents that, for any "x" of type "nat", "x+1" and "1+x" are equal. And a term of that