Nuprl - Proof: comp preserves surj

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Composing surjections gives a surjection.

A,B,C:Type, g:(A

B), f:(B

C).

Surj(A; B; g)

Surj(B; C; f)

Surj(A; C; f o g)

By:	Def of Surj(<A>; <B>; <f>)

Generated subgoal:

1 1. A : Type
2. B : Type
3. C : Type
4. g : AB
5. f : BC
6. b:B. a:A. g(a) = b
7. c:C. b:B. f(b) = c
8. c : C
a:A. (f o g)(a) = c
5 steps

About:

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