---

Step * 1 1 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. g : (x,y:A//E[x;y]) ⟶ A
6. ∀c:x,y:A//E[x;y]. ((g c) = c ∈ (x,y:A//E[x;y]))
7. f : (x,y:A//E[x;y]) ⟶ B
8. Inj(x,y:A//E[x;y];B;f)
9. Surj(x,y:A//E[x;y];B;f)
⊢ A ~ B mod (a1,a2.E[a1;a2])
BY
{ (D 0 With ⌜f⌝  THEN Auto) }

1
1. [A] : Type
2. [B] : Type
3. E : A ⟶ A ⟶ ℙ
4. [%] : EquivRel(A;x,y.E[x;y])
5. g : (x,y:A//E[x;y]) ⟶ A
6. ∀c:x,y:A//E[x;y]. ((g c) = c ∈ (x,y:A//E[x;y]))
7. f : (x,y:A//E[x;y]) ⟶ B
8. Inj(x,y:A//E[x;y];B;f)
9. Surj(x,y:A//E[x;y];B;f)
⊢ Surj(A;B;f)

2
1. A : Type
2. B : Type
3. E : A ⟶ A ⟶ ℙ
4. EquivRel(A;x,y.E[x;y])
5. g : (x,y:A//E[x;y]) ⟶ A
6. ∀c:x,y:A//E[x;y]. ((g c) = c ∈ (x,y:A//E[x;y]))
7. f : (x,y:A//E[x;y]) ⟶ B
8. Inj(x,y:A//E[x;y];B;f)
9. Surj(x,y:A//E[x;y];B;f)
10. Surj(A;B;f)
11. a1 : A
12. a2 : A
13. (f a1) = (f a2) ∈ B
⊢ ↓E[a1;a2]

3
1. A : Type
2. B : Type
3. E : A ⟶ A ⟶ ℙ
4. EquivRel(A;x,y.E[x;y])
5. g : (x,y:A//E[x;y]) ⟶ A
6. ∀c:x,y:A//E[x;y]. ((g c) = c ∈ (x,y:A//E[x;y]))
7. f : (x,y:A//E[x;y]) ⟶ B
8. Inj(x,y:A//E[x;y];B;f)
9. Surj(x,y:A//E[x;y];B;f)
10. Surj(A;B;f)
11. a1 : A
12. a2 : A
13. E[a1;a2]
⊢ (f a1) = (f a2) ∈ B

---

Latex:

---

Latex:

1.  [A]  :  Type
2.  [B]  :  Type
3.  E  :  A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}
4.  [\%]  :  EquivRel(A;x,y.E[x;y])
5.  g  :  (x,y:A//E[x;y])  {}\mrightarrow{}  A
6.  \mforall{}c:x,y:A//E[x;y].  ((g  c)  =  c)
7.  f  :  (x,y:A//E[x;y])  {}\mrightarrow{}  B
8.  Inj(x,y:A//E[x;y];B;f)
9.  Surj(x,y:A//E[x;y];B;f)
\mvdash{}  A  \msim{}  B  mod  (a1,a2.E[a1;a2])


By

---

Latex:
(D  0  With  \mkleeneopen{}f\mkleeneclose{}    THEN  Auto)

---

Home Index