---

Step * of Lemma quotient-equipollent

∀[A,B:Type].
  (finite-type(A)
  ⇒ (∀x,y:B.  Dec(x = y ∈ B))
  ⇒ (∀E:A ⟶ A ⟶ ℙ. x,y:A//E[x;y] ~ B ⇐⇒ A ~ B mod (a1,a2.E[a1;a2]) supposing EquivRel(A;x,y.E[x;y])))
BY
{ (InstLemma `equiv-equipollent-iff-quotient-equipollent` []
   THEN RepeatFor 2 (ParallelLast')
   THEN RepeatFor 2 ((D 0 THENA Auto))
   THEN (ParallelOp 3 THEN ParallelLast)
   THEN D -1
   THEN Auto) }

1
.....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)))

---

Latex:

---

Latex:
\mforall{}[A,B:Type].
    (finite-type(A)
    {}\mRightarrow{}  (\mforall{}x,y:B.    Dec(x  =  y))
    {}\mRightarrow{}  (\mforall{}E:A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}
                x,y:A//E[x;y]  \msim{}  B  \mLeftarrow{}{}\mRightarrow{}  A  \msim{}  B  mod  (a1,a2.E[a1;a2])  supposing  EquivRel(A;x,y.E[x;y])))


By

---

Latex:
(InstLemma  `equiv-equipollent-iff-quotient-equipollent`  []
  THEN  RepeatFor  2  (ParallelLast')
  THEN  RepeatFor  2  ((D  0  THENA  Auto))
  THEN  (ParallelOp  3  THEN  ParallelLast)
  THEN  D  -1
  THEN  Auto)

---

Home Index