At: inv funs 2 unique

  A,B:Type, f:(AB), g,h:(BA).
  InvFuns(A;B;f;g)  InvFuns(A;B;f;h)  g = h

1

1. A : Type 2. B : Type 3. f : AB 4. g : BA 5. h : BA 6. x:A. g(f(x)) = x 7. y:B. f(g(y)) = y 8. x:A. h(f(x)) = x 9. y:B. f(h(y)) = y   g = h

2 steps

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