At: invfuns are inj

  A,B:Type, f:(AB), g:(BA).
  InvFuns(A;B;f;g)  Inj(A; B; f) & Inj(B; A; g)

1

1. A : Type 2. B : Type 3. f : AB 4. g : BA 5. InvFuns(A;B;f;g)   Inj(A; B; f) & Inj(B; A; g)

3 steps

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