Editing Type theory (section)

=== Type constructors ===
Some type theories allow for types of complex terms, such as functions or lists, to depend on the types of its arguments; these are called [[Kind (type theory)|type constructors]]. For example, a type theory could have the dependent type <math>\mathsf{list}\,a</math>, which should correspond to [[List (abstract data type)|lists]] of terms, where each term must have type <math>a</math>. In this case, <math>\mathsf{list}</math> has the kind <math>U\to U</math>, where <math>U</math> denotes the [[Universe (mathematics)|universe]] of all types in the theory. 

====Product type====
The product type, <math>\times</math>, depends on two types, and its terms are commonly written as [[Ordered pair|ordered pairs]] <math>(s,t)</math>. The pair <math>(s,t)</math> has the product type <math>\sigma\times\tau</math>, where <math>\sigma</math> is the type of <math>s</math> and <math>\tau</math> is the type of <math>t</math>. Each product type is then usually defined with eliminator functions <math>\mathrm{first}:\sigma\times\tau\to\sigma</math> and <math>\mathrm{second}:\sigma\times\tau\to\tau</math>.

* <math>\mathrm{first}\,(s,t)</math> returns <math>s</math>, and
* <math>\mathrm{second}\,(s,t)</math> returns <math>t</math>.

Besides ordered pairs, this type is used for the concepts of [[logical conjunction]] and [[intersection]].

====Sum type====
The sum type is written as either <math>+</math> or <math>\sqcup</math>. In programming languages, sum types may be referred to as [[Tagged union|tagged unions]]. Each type <math>\sigma\sqcup\tau</math> is usually defined with [[Constructor (programming)|constructors]] <math>\mathrm{left}:\sigma\to(\sigma\sqcup\tau)</math> and <math>\mathrm{right}:\tau\to(\sigma\sqcup\tau)</math>, which are [[Injective function|injective]], and an eliminator function <math>\mathrm{match}:(\sigma\to\rho)\to(\tau\to\rho)\to(\sigma\sqcup\tau)\to\rho</math> such that

* <math>\mathrm{match}\,f\,g\,(\mathrm{left}\,x)</math> returns <math>f\,x</math>, and
* <math>\mathrm{match}\,f\,g\,(\mathrm{right}\,y)</math> returns <math>g\,y</math>.

The sum type is used for the concepts of [[logical or|logical disjunction]] and [[Union (set theory)|union]].