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))
19. u : A
  InvFuns(B(u);B''(f1(f(u)));F1(f(u)) o F(u);G(u) o G1(f(u)))

1

20. x:B(u). G(u,F(u,x)) = x 21. y:B'(f(u)). F(u,G(u,y)) = y 22. x:B'(f(u)). G1(f(u),F1(f(u),x)) = x 23. y:B''(f1(f(u))). F1(f(u),G1(f(u),y)) = y   InvFuns(B(u);B''(f1(f(u)));F1(f(u)) o F(u);G(u) o G1(f(u)))

3 steps

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