 All entities have types, and if α and β are types, the type of functions from elements of type β to elements of type α is written as \((\alpha \beta)\). (This notation was introduced by Church, but some authors write \((\beta \rightarrow \alpha)\) instead of \((\alpha \beta)\). See, for example, Section 2 of the entry on  type theory.)