#
Homotopy Type Theory

function type (Rev #1)

## Idea

## 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$.

## Properties

## References

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.