---

Step * of Lemma equiv-equipollent-iff-quotient-equipollent

∀[A,B:Type].
  ∀E:A ⟶ A ⟶ ℙ
    ((∃g:(x,y:A//E[x;y]) ⟶ A. ∀c:x,y:A//E[x;y]. ((g c) = c ∈ (x,y:A//E[x;y])))
    ∨ (∀f:A ⟶ B. ∀b:B.  SqStable(∃a:A. ((f a) = b ∈ B))))
    ⇒ (A ~ B mod (a1,a2.E[a1;a2]) ⇐⇒ x,y:A//E[x;y] ~ B) 
    supposing EquivRel(A;x,y.E[x;y])
BY
{ (EAuto 1 THEN D -2 THEN ExRepD) }

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. x,y:A//E[x;y] ~ B
⊢ A ~ B mod (a1,a2.E[a1;a2])

2
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. x,y:A//E[x;y] ~ B
⊢ A ~ B mod (a1,a2.E[a1;a2])

---

Latex:

---

Latex:
\mforall{}[A,B:Type].
    \mforall{}E:A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}
        ((\mexists{}g:(x,y:A//E[x;y])  {}\mrightarrow{}  A.  \mforall{}c:x,y:A//E[x;y].  ((g  c)  =  c))
        \mvee{}  (\mforall{}f:A  {}\mrightarrow{}  B.  \mforall{}b:B.    SqStable(\mexists{}a:A.  ((f  a)  =  b))))
        {}\mRightarrow{}  (A  \msim{}  B  mod  (a1,a2.E[a1;a2])  \mLeftarrow{}{}\mRightarrow{}  x,y:A//E[x;y]  \msim{}  B) 
        supposing  EquivRel(A;x,y.E[x;y])


By

---

Latex:
(EAuto  1  THEN  D  -2  THEN  ExRepD)

---

Home Index