f:(A
B), g:(BA). InvFuns(A; B; f; g)
Thm* 
A,B:Type. (A ~ B) 
Prop
Thm* A,B:Type, f:(AB), g:(BA). InvFuns(A; B; f; g) Prop
Thm* A:Type. Id AA
Thm* A,B,C:Type, f:(BC), g:(AB). f o g AC
Thm* A:Type. Id AA
| one_one_corr |
Def A ~ B == f:(AB), g:(BA). InvFuns(A; B; f; g)
Thm* |
| inv_funs |
Def InvFuns(A; B; f; g) == g o f = Id & f o g = Id
Thm* |
| tidentity |
Def Id == Id
Thm* |
| compose |
Def (f o g)(x) == f(g(x))
Thm* |
| identity |
Def Id(x) == x
Thm* |
About:
 |  |  |  |  |
 |  |  |  |  |