2. B: Type
3. C: Type
4. f1: A
B5. g1: B
A6. InvFuns(A; B; f1; g1)
7. f: B
C8. g: C
B9. InvFuns(B; C; f; g)
f:(AC), g:(CA). InvFuns(A; C; f; g) 
A,B,C:Type. (A ~ B) 
(B ~ C) (A ~ C)| 1 | 1. A: Type 2. B: Type 3. C: Type 4. f1: A B5. g1: B A6. InvFuns(A; B; f1; g1) 7. f: B C8. g: C B9. InvFuns(B; C; f; g) f:(AC), g:(CA). InvFuns(A; C; f; g) |
About:
 |  |  |  |  |