Homotopy Type Theory function type > history (Rev #2, changes)

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

Idea

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:

(λ x . y) z a \equiv y [x a / z x]

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

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

~~Properties~~

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))

Revision on January 19, 2019 at 15:22:54 by Ali Caglayan. See the history of this page for a list of all contributions to it.