1. A : Type
2. A Discrete
3. k : 
4. f : kA
5. Inj(k; A; f)
6. {a:A| i:k. a = f(i) }  Type
7. f  k{a:A| i:k. a = f(i) } & Surj(k; {a:A| i:k. a = f(i) }; f)
8. {a:A| i:k. a = f(i) }  Type
9. f  k{a:A| i:k. a = f(i) }
10. Surj(k; {a:A| i:k. a = f(i) }; f)
11. f  k{a:A| i:k. a = f(i) }
  Inj(k; {a:A| i:k. a = f(i) }; f)

None

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