Showing changes from revision #2 to #3:
Added | Removed | Changed
Let be two types. We introduce a type called the function type. The constructors for this type are written as
where and .
These can be computed (on application) using -reduction:
which says take and replace all occurrences of with for an .
Given any type , there is a function called the identity function of denoted and defined by
Given any types and two functions , the composition of and is the function
Last revised on June 9, 2022 at 20:46:39. See the history of this page for a list of all contributions to it.