---

Step * 1 1 of Lemma equiv-equipollent-implies-quotient-equipollent


1. [A] : Type
2. [B] : Type
3. E : A ⟶ A ⟶ ℙ
4. A ~ B mod (a1,a2.E[a1;a2])
5. EquivRel(A;x,y.↓E[x;y])
⊢ x,y:A//(↓E[x;y]) ~ B
BY
{ (D -2 THEN ExRepD) }

1
1. [A] : Type
2. [B] : Type
3. E : A ⟶ A ⟶ ℙ
4. f : A ⟶ B
5. Surj(A;B;f)
6. ∀a1,a2:A.  ((f a1) = (f a2) ∈ B ⇐⇒ ↓E[a1;a2])
7. EquivRel(A;x,y.↓E[x;y])
⊢ x,y:A//(↓E[x;y]) ~ B

---

Latex:

---

Latex:

1.  [A]  :  Type
2.  [B]  :  Type
3.  E  :  A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}
4.  A  \msim{}  B  mod  (a1,a2.E[a1;a2])
5.  EquivRel(A;x,y.\mdownarrow{}E[x;y])
\mvdash{}  x,y:A//(\mdownarrow{}E[x;y])  \msim{}  B


By

---

Latex:
(D  -2  THEN  ExRepD)

---

Home Index