Homotopy Type Theory function type > history (Rev #1)

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

which says take yy and replace all occurrences of xx with zz.

Properties

References

category: type theory

Revision on October 11, 2018 at 12:50:29 by Ali Caglayan. See the history of this page for a list of all contributions to it.