Editing Type theory (section)

==Differences from set theory==
The most commonly accepted [[Foundations of mathematics|foundation for mathematics]] is [[first-order logic]] with the [[Formal language|language]] and [[Axiom|axioms]] of [[Zermelo–Fraenkel set theory]] with the [[axiom of choice]], abbreviated ZFC. Type theories having sufficient [[Expressive power (computer science)|expressibility]] may also act as a foundation of mathematics. There are a number of differences between these two approaches.

* Set theory has both [[Rule of inference|rules]] and [[axiom]]s, while type theories only have rules. Type theories, in general, do not have axioms and are defined by their rules of inference.<ref name=":5" />
* Classical set theory and logic have the [[law of excluded middle]]. When a type theory encodes the concepts of "and" and "or" as types, it leads to [[intuitionistic logic]], and does not necessarily have the law of excluded middle.<ref name=":3" />
* In set theory, an element is not restricted to one set. The element can appear in subsets and unions with other sets. In type theory, terms (generally) belong to only one type. Where a subset would be used, type theory can use a [[Predicate (mathematical logic)|predicate function]] or use a dependently-typed product type, where each element <math>x</math> is paired with a proof that the subset's property holds for <math>x</math>. Where a union would be used, type theory uses the sum type, which contains new canonical terms.
* Type theory has a built-in notion of computation. Thus, "1+1" and "2" are different terms in type theory, but they compute to the same value. Moreover, functions are defined computationally as lambda terms. In set theory, "1+1=2" means that "1+1" is just another way to refer the value "2". Type theory's computation does require a complicated concept of equality.
* Set theory [[Set-theoretic definition of natural numbers|encodes numbers as sets]]. Type theory can encode numbers as functions using [[Church encoding]], or more naturally as [[Intuitionistic type theory#Inductive types|inductive types]], and the construction closely resembles [[Peano axioms|Peano's axioms]].
* In type theory, proofs are types whereas in set theory, proofs are part of the underlying first-order logic.<ref name=":5" />

Proponents of type theory will also point out its connection to constructive mathematics through the [[BHK interpretation]], its connection to logic by the [[Curry–Howard isomorphism]], and its connections to [[Category theory]].

===Properties of type theories===
Terms usually belong to a single type. However, there are set theories that define "subtyping".

Computation takes place by repeated application of rules. Many types of theories are [[strongly normalizing]], which means that any order of applying the rules will always end in the same result. However, some are not. In a normalizing type theory, the one-directional computation rules are called "reduction rules", and applying the rules "reduces" the term. If a rule is not one-directional, it is called a "conversion rule".

Some combinations of types are equivalent to other combinations of types. When functions are considered "exponentiation", the combinations of types can be written similarly to algebraic identities.<ref name=":4">{{cite web|last1=Milewski|first1=Bartosz|title=Programming with Math (Exploring Type Theory)|url=https://www.youtube.com/watch?v=8AGWTWVOJ74|website=YouTube|access-date=2022-01-22|archive-date=2022-01-22|archive-url=https://web.archive.org/web/20220122213434/https://www.youtube.com/watch?v=8AGWTWVOJ74|url-status=live}}</ref> Thus, <math>{\mathbb 0} + A \cong A</math>, <math>{\mathbb 1} \times A \cong A</math>, <math>{\mathbb 1} + {\mathbb 1} \cong {\mathbb 2}</math>, <math>A^{B+C} \cong A^B \times A^C</math>, <math>A^{B\times C} \cong (A^B)^C</math>.

===Axioms===
Most type theories do not have [[axiom]]s. This is because a type theory is defined by its rules of inference. This is a source of confusion for people familiar with Set Theory, where a theory is defined by both the rules of inference for a logic (such as [[first-order logic]]) and axioms about sets.

Sometimes, a type theory will add a few axioms. An axiom is a judgment that is accepted without a derivation using the rules of inference. They are often added to ensure properties that cannot be added cleanly through the rules.

Axioms can cause problems if they introduce terms without a way to compute on those terms. That is, axioms can interfere with the [[Normal form (abstract rewriting)|normalizing property]] of the type theory.<ref>{{cite web|title=Axioms and Computation|url=https://leanprover.github.io/theorem_proving_in_lean/axioms_and_computation.html|website=Theorem Proving in Lean|access-date=21 January 2022|archive-date=22 December 2021|archive-url=https://web.archive.org/web/20211222130219/https://leanprover.github.io/theorem_proving_in_lean/axioms_and_computation.html|url-status=live}}</ref>

Some commonly encountered axioms are:
* "Axiom K" ensures "uniqueness of identity proofs". That is, that every term of an identity type is equal to reflexivity.<ref>{{cite web|title=Axiom K|url=http://nlab-pages.s3.us-east-2.amazonaws.com/nlab/show/axiom+K+(type+theory)|website=nLab|access-date=2022-01-21|archive-date=2022-01-19|archive-url=https://web.archive.org/web/20220119172036/http://nlab-pages.s3.us-east-2.amazonaws.com/nlab/show/axiom+K+(type+theory)|url-status=live}}</ref>
* "Univalence Axiom" holds that equivalence of types is equality of types. The research into this property led to [[cubical type theory]], where the property holds without needing an axiom.<ref name=":0">{{cite journal|last1=Cohen|first1=Cyril|last2=Coquand|first2=Thierry|last3=Huber|first3=Simon|last4=Mörtberg|first4=Anders|title=Cubical Type Theory: A constructive interpretation of the univalence axiom|journal=21st International Conference on Types for Proofs and Programs (TYPES 2015)|date=2016|doi=10.4230/LIPIcs.CVIT.2016.23|doi-broken-date=1 November 2024|doi-access=free |arxiv=1611.02108|url=https://www.cse.chalmers.se/~simonhu/papers/cubicaltt.pdf|archive-url=https://ghostarchive.org/archive/20221009/https://www.cse.chalmers.se/~simonhu/papers/cubicaltt.pdf|archive-date=2022-10-09|url-status=live}}</ref>
* "Law of Excluded Middle" is often added to satisfy users who want [[classical logic]], instead of intuitionistic logic.

The [[Axiom of choice|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 mathematics|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 {{Section link|Axiom of choice#In constructive mathematics}}.)