At: bij imp exists inv version2

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

1

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

8 steps

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