---

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


1. [A] : Type
2. [B] : Type
3. E : A ⟶ A ⟶ ℙ
4. [%] : EquivRel(A;x,y.E[x;y])
5. A ~ B mod (a1,a2.E[a1;a2])
6. x,y:A//E[x;y] ~ x,y:A//(↓E[x;y])
7. EquivRel(A;x,y.↓E[x;y])
⊢ x,y:A//E[x;y] ~ B
BY
{ ((RWO "-2" 0 THENA Auto) THEN Thin (-2) THEN Thin (-3)) }

1
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

---

Latex:

---

Latex:

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


By

---

Latex:
((RWO  "-2"  0  THENA  Auto)  THEN  Thin  (-2)  THEN  Thin  (-3))

---

Home Index