A:Type. 
  (A Discrete)
  
  (k:, f:(kA).
  ({a:A| i:k. a = f(i) }  Type
  (& f  k{a:A| i:k. a = f(i) }
  (& Surj(k; {a:A| i:k. a = f(i) }; f))

1

1. A : Type 2. A Discrete 3. k :  4. f : kA   {a:A| i:k. a = f(i) }  Type   & f  k{a:A| i:k. a = f(i) }   & Surj(k; {a:A| i:k. a = f(i) }; f)

15 steps

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