A,B:Type, f:(A
B), 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 inv funs? | |
| 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: | InvFuns(A; B; f; g) | has structure: | inv_funs(A; B; f; g) |
About:
 |  |  |  |  |  |  |  |  |