At: left inv of surj is right inv

  A,B:Type, f:(AB), g:(BA).
  Surj(A; B; f)  (x:A. g(f(x)) = x)  (y:B. f(g(y)) = y)

1

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

3 steps

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