Homotopy Type Theory
function type > history (Rev #3, changes)
Showing changes from revision #2 to #3:
Added | Removed | Changed
Idea
< function type
Definition
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
References
Revision on June 9, 2022 at 20:46:39 by
Anonymous?.
See the history of this page for a list of all contributions to it.