At: surj is inj gen 1 1 1 1 2 1 1 1 1 1 1 1 1 1 1 1 1 1
1. A: Type
2. B: Type
3. f: A
B
4. f1: AB
5. g: BA
6. g o f1 = Id
7. f1 o g = Id
8. n: 
9. f2: nB
10. g1: Bn
11. g1 o f2 = Id
12. f2 o g1 = Id
13. Surj(A; B; f)
14. a1: A
15. a2: A
16. f(a1) = f(a2)
g1(f(a1)) = g1(f(a2))
By: RWH (HypC 16) 0
Generated subgoals:None
About:
