1. A : Type
2. A' : Type
3. A'' : Type
4. B : AType
5. B' : A'Type
6. B'' : A''Type
7. f : AA'
8. g : A'A
9. F : x:AB(x)B'(f(x))
10. G : x:AB'(f(x))B(x)
11. InvFuns(A;A';f;g)
12. u:A. InvFuns(B(u);B'(f(u));F(u);G(u))
13. f1 : A'A''
14. g1 : A''A'
15. F1 : x':A'B'(x')B''(f1(x'))
16. G1 : x':A'B''(f1(x'))B'(x')
17. InvFuns(A';A'';f1;g1)
18. u:A'. InvFuns(B'(u);B''(f1(u));F1(u);G1(u))
  InvFuns(A;A'';f1 o f;g o g1)

1

19. x:A'. g1(f1(x)) = x 20. y:A''. f1(g1(y)) = y 21. x:A. g(f(x)) = x 22. y:A'. f(g(y)) = y   InvFuns(A;A'';f1 o f;g o g1)

3 steps

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html