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