#
Homotopy Type Theory
function type > history (changes)

Showing changes from revision #2 to #3:
Added | ~~Removed~~ | ~~Chan~~ged

## Idea

< function type

## 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)a \equiv y[a/x]$

~~
~~which says take $y$ and replace all occurrences of $x$ with $a$ for an $a : A$.

~~
~~Given any type $A$, there is a function called the *identity function* of $A$ denoted and defined by

~~
~~$id_A : A \to A$

$id_A \equiv \lambda x.x$

~~
~~Given any types $A,B,C$ and two functions $f : A \to B$, $g : B \to C$ the composition of $f$ and $g$ is the function

~~
~~$g \circ f : A \to C$

$(g \circ f) (x) \equiv g(f(x))$

~~
~~## References

~~
~~~~
~~
Last revised on June 9, 2022 at 20:46:39.
See the history of this page for a list of all contributions to it.