---

Step * 1 of Lemma quotient-equipollent

.....antecedent..... 
1. [A] : Type
2. [B] : Type
3. ∀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])
4. finite-type(A)
5. ∀x,y:B.  Dec(x = y ∈ B)
6. E : A ⟶ A ⟶ ℙ
7. [%6] : EquivRel(A;x,y.E[x;y])
⊢ (∃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)))
BY
{ (OrRight THEN EAuto 1) }

---

Latex:

---

Latex:
.....antecedent..... 
1.  [A]  :  Type
2.  [B]  :  Type
3.  \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])
4.  finite-type(A)
5.  \mforall{}x,y:B.    Dec(x  =  y)
6.  E  :  A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}
7.  [\%6]  :  EquivRel(A;x,y.E[x;y])
\mvdash{}  (\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)))


By

---

Latex:
(OrRight  THEN  EAuto  1)

---

Home Index