Homotopy Type Theory
function type

Idea

Definition

Let A,BA,B be two types. We introduce a type ABA \to B called the function type. The constructors for this type are written as

(λx.y):AB(\lambda x . y) : A \to B

where x:Ax:A and y:By:B.

These can be computed (on application) using β\beta-reduction:

(λx.y)ay[a/x](\lambda x. y)a \equiv y[a/x]

which says take yy and replace all occurrences of xx with aa for an a:Aa : A.

Given any type AA, there is a function called the identity function of AA denoted and defined by

id A:AAid_A : A \to A
id Aλx.x id_A \equiv \lambda x.x

Given any types A,B,CA,B,C and two functions f:ABf : A \to B, g:BCg : B \to C the composition of ff and gg is the function

gf:ACg \circ f : A \to C
(gf)(x)g(f(x)) (g \circ f) (x) \equiv g(f(x))

References

category: type theory