A,B:Type, f:(A
B). Bij(A; B; f) 
Prop
PA:Prop. Dec(A) PropA:Type. Id AA| 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 | |
| decidable | Def Dec(P) == P P |
| Thm* A:Prop. Dec(A) Prop | |
| tidentity | Def Id == Id |
| Thm* A:Type. Id AA |
About:
 |  |  |  |  |  |  |  |  |