---

Step * 2 1 3 of Lemma equiv-equipollent-iff-quotient-equipollent


1. A : Type
2. B : Type
3. E : A ⟶ A ⟶ ℙ
4. EquivRel(A;x,y.E[x;y])
5. ∀f:A ⟶ B. ∀b:B.  SqStable(∃a:A. ((f a) = b ∈ B))
6. f : (x,y:A//E[x;y]) ⟶ B
7. Inj(x,y:A//E[x;y];B;f)
8. Surj(x,y:A//E[x;y];B;f)
9. Surj(A;B;f)
10. a1 : A
11. a2 : A
12. E[a1;a2]
⊢ (f a1) = (f a2) ∈ B
BY
{ ((EqCD THEN Auto) THEN EqTypeCD THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  E  :  A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}
4.  EquivRel(A;x,y.E[x;y])
5.  \mforall{}f:A  {}\mrightarrow{}  B.  \mforall{}b:B.    SqStable(\mexists{}a:A.  ((f  a)  =  b))
6.  f  :  (x,y:A//E[x;y])  {}\mrightarrow{}  B
7.  Inj(x,y:A//E[x;y];B;f)
8.  Surj(x,y:A//E[x;y];B;f)
9.  Surj(A;B;f)
10.  a1  :  A
11.  a2  :  A
12.  E[a1;a2]
\mvdash{}  (f  a1)  =  (f  a2)


By

---

Latex:
((EqCD  THEN  Auto)  THEN  EqTypeCD  THEN  Auto)

---

Home Index