Homotopy Type Theory function type (Rev #1)

Definition

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

$(\lambda x . y) : A \to B$

where $x:A$ and $y:B$.

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

$(\lambda x. y)z \equiv y[x/z]$

which says take $y$ and replace all occurrences of $x$ with $z$.

References

category: type theory

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