Homotopy Type Theory
function type (changes)

Showing changes from revision #1 to #2: Added | Removed | Changed



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) z ay[ x a/ z x] (\lambda x. y)z y)a \equiv y[x/z] y[a/x]

which says take yy and replace all occurrences of xx with z a z a 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))


category: type theory

Last revised on January 19, 2019 at 10:22:54. See the history of this page for a list of all contributions to it.