A,A',B,B':Type. (A ~ A')  (B ~ B')  ((A+B) ~ (A'+B'))

1

1. A : Type 2. A' : Type 3. B : Type 4. B' : Type 5. f:(AA'), g:(A'A). InvFuns(A;A';f;g) 6. f:(BB'), g:(B'B). InvFuns(B;B';f;g)   f:((A+B)(A'+B')), g:((A'+B')(A+B)). InvFuns(A+B;A'+B';f;g)

6 steps

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