---

Step * of Lemma CCC-surjection

∀[A,B:Type].  ((∃f:A ⟶ B. Surj(A;B;f)) ⇒ CCC(A) ⇒ CCC(B))
BY
{ (Auto
   THEN ExRepD
   THEN ParallelLast
   THEN Auto
   THEN (D -3 With ⌜λn,a. (R n (f a))⌝  THENA Auto)
   THEN Reduce -1
   THEN (D -1 THENA (Auto THEN (D -2 With ⌜f o g⌝  THENA Auto) THEN Reduce -1 THEN Auto))
   THEN ParallelLast
   THEN Auto
   THEN (D 4 With ⌜m⌝  THENA Auto)
   THEN D -1
   THEN RWO "-1<" 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A,B:Type].    ((\mexists{}f:A  {}\mrightarrow{}  B.  Surj(A;B;f))  {}\mRightarrow{}  CCC(A)  {}\mRightarrow{}  CCC(B))


By

---

Latex:
(Auto
  THEN  ExRepD
  THEN  ParallelLast
  THEN  Auto
  THEN  (D  -3  With  \mkleeneopen{}\mlambda{}n,a.  (R  n  (f  a))\mkleeneclose{}    THENA  Auto)
  THEN  Reduce  -1
  THEN  (D  -1  THENA  (Auto  THEN  (D  -2  With  \mkleeneopen{}f  o  g\mkleeneclose{}    THENA  Auto)  THEN  Reduce  -1  THEN  Auto))
  THEN  ParallelLast
  THEN  Auto
  THEN  (D  4  With  \mkleeneopen{}m\mkleeneclose{}    THENA  Auto)
  THEN  D  -1
  THEN  RWO  "-1<"  0
  THEN  Auto)

---

Home Index