1. A : Type
2. B : Type
3. f : AB
4. a1,a2:A. f(a1) = f(a2)  a1 = a2
5. f1:(BA). b:B. f(f1(b)) = b
  g:(BA). InvFuns(A; B; f; g)

1

5. g : BA 6. b:B. f(g(b)) = b   g:(BA). InvFuns(A; B; f; g)

8 steps

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