Showing changes from revision #6 to #7:
Added | Removed | Changed
Given types and and a subtype with inclusion? in a universe , a partial function with domain and codomain is simply a function .
The type of partial functions with domain and codomain in a universe , , is defined as
A partial function could also be directly defined as a function , where is the partial function classifier of . The type of partial functions here is simply the function type .
Every partial function between two sets and has an associated functional relation