fun_1 Theory

Variatns 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 polymorhic types as well as it should).

Summary of Definitions

Typed Definitions

tlambda *

identity *1

tidentity *1

compose *1

inv_funs *1

one_one_corr *1

inject *1

surject *1

biject *1

Main Theorems

eta_conv *3

comp_assoc *5

comp_id_l *5

comp_id_r *6

sq_stable__inv_funs *4

sq_stable__inject *1

ax_choice *11

dep_ax_choice *11

inv_funs_sym *2

bij_imp_exists_inv *21

fun_with_inv_is_bij *18

bij_iff_1_1_corr *10