IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
fun_1
Nuprl Section: fun_1
Definitions are introduced for polymorphic identity and composition functions, and for predicates such as injectivity and surjectivity.
Basic properties of the functions are proven, as are inter-relationships between the predicates.
Variants on lambda abstraction and the identity function are introduced that include type tags that vanish when the definitions are unfolded. Use of these type tags is encouraged, since the type inference routines sometimes have difficulties without them (the current type inference routine works on terms bottom up, and doesn't handle polymorphic types as well as it should).
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html