f:(A
B), g:(BA). InvFuns(A; B; f; g)
A,B:Type. (A ~~ B) 
PropA,B:Type, f:(AB), g:(BA). InvFuns(A; B; f; g) PropA:Type. Id AAA,B,C:Type, f:(BC), g:(AB). f o g ACA:Type. Id AA| Who Cites one one corr? | |
| one_one_corr | Def A ~~ B == f:(AB), g:(BA). InvFuns(A; B; f; g) |
| Thm* A,B:Type. (A ~~ B) Prop | |
| inv_funs | Def InvFuns(A; B; f; g) == g o f = Id & f o g = Id |
| Thm* A,B:Type, f:(AB), g:(BA). InvFuns(A; B; f; g) Prop | |
| tidentity | Def Id == Id |
| Thm* A:Type. Id AA | |
| compose | Def (f o g)(x) == f(g(x)) |
| Thm* A,B,C:Type, f:(BC), g:(AB). f o g AC | |
| identity | Def Id(x) == x |
| Thm* A:Type. Id AA |
| Syntax: | A ~~ B | has structure: | one_one_corr(A; B) |
About:
 |  |  |  |  |  |
 |  |  |  |