A,B:Type, f:(A
B). Bij(A; B; f) 
PropA:Type. Id AAa1,a2:A. f(a1) = f(a2) B 
a1 = a2A,B:Type, f:(AB). Inj(A; B; f) Propb:B. 
a:A. f(a) = bA,B:Type, f:(AB). Surj(A; B; f) Prop| Some definitions of interest. | |
| biject | Def Bij(A; B; f) == Inj(A; B; f) & Surj(A; B; f) |
| Thm* A,B:Type, f:(AB). Bij(A; B; f) Prop | |
| identity | Def Id(x) == x |
| Thm* A:Type. Id AA | |
| inject | Def Inj(A; B; f) == a1,a2:A. f(a1) = f(a2) B a1 = a2 |
| Thm* A,B:Type, f:(AB). Inj(A; B; f) Prop | |
| surject | Def Surj(A; B; f) == b:B. a:A. f(a) = b |
| Thm* A,B:Type, f:(AB). Surj(A; B; f) Prop |
About:
 |  |  |  |  |  |
 |  |  |  |
 |