---

Step * 1 2 of Lemma equipollent-quotient2


1. [A] : Type
2. E : A ⟶ A ⟶ ℙ
3. d : ∀x,y:A.  Dec(↓E[x;y])
4. EquivRel(A;x,y.↓E[x;y])
5. ∀x,y:A.  (isl(d x y) ∈ 𝔹)
6. ∀x,y:A.  (↑isl(d x y) ⇐⇒ ↓E[x;y])
7. A ~ a:x,y:A//(↑isl(d x y)) × {b:A| ↑isl(d a b)} 
8. EquivRel(A;x,y.↑isl(d x y))
9. x,y:A//(↓E[x;y]) ≡ x,y:A//(↑isl(d x y))
⊢ A ~ a:x,y:A//(↓E[x;y]) × {b:A| ↑isl(d a b)} 
BY
{ ((Assert a:x,y:A//(↑isl(d x y)) × {b:A| ↑isl(d a b)}  ∈ Type BY
          (MemCD
           THEN Try (Complete (Auto))
           THEN (Subst' {b:A| ↑isl(d a b)}  ~ equiv-class(A;a,b.isl(d a b);a) 0 THENA (RepUR ``equiv-class`` 0 THEN Auto\000C))
           THEN Auto))
   THEN (Assert a:x,y:A//(↓E[x;y]) × {b:A| ↑isl(d a b)}  ∈ Type BY
               (MemCD
                THEN Try (Complete (Auto))
                THEN (Subst' {b:A| ↑isl(d a b)}  ~ equiv-class(A;a,b.isl(d a b);a) 0 THENA (RepUR ``equiv-class`` 0 THEN\000C Auto))
                THEN Auto))
   ) }

1
1. [A] : Type
2. E : A ⟶ A ⟶ ℙ
3. d : ∀x,y:A.  Dec(↓E[x;y])
4. EquivRel(A;x,y.↓E[x;y])
5. ∀x,y:A.  (isl(d x y) ∈ 𝔹)
6. ∀x,y:A.  (↑isl(d x y) ⇐⇒ ↓E[x;y])
7. A ~ a:x,y:A//(↑isl(d x y)) × {b:A| ↑isl(d a b)} 
8. EquivRel(A;x,y.↑isl(d x y))
9. x,y:A//(↓E[x;y]) ≡ x,y:A//(↑isl(d x y))
10. a:x,y:A//(↑isl(d x y)) × {b:A| ↑isl(d a b)}  ∈ Type
11. a:x,y:A//(↓E[x;y]) × {b:A| ↑isl(d a b)}  ∈ Type
⊢ A ~ a:x,y:A//(↓E[x;y]) × {b:A| ↑isl(d a b)} 

---

Latex:

---

Latex:

1.  [A]  :  Type
2.  E  :  A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}
3.  d  :  \mforall{}x,y:A.    Dec(\mdownarrow{}E[x;y])
4.  EquivRel(A;x,y.\mdownarrow{}E[x;y])
5.  \mforall{}x,y:A.    (isl(d  x  y)  \mmember{}  \mBbbB{})
6.  \mforall{}x,y:A.    (\muparrow{}isl(d  x  y)  \mLeftarrow{}{}\mRightarrow{}  \mdownarrow{}E[x;y])
7.  A  \msim{}  a:x,y:A//(\muparrow{}isl(d  x  y))  \mtimes{}  \{b:A|  \muparrow{}isl(d  a  b)\} 
8.  EquivRel(A;x,y.\muparrow{}isl(d  x  y))
9.  x,y:A//(\mdownarrow{}E[x;y])  \mequiv{}  x,y:A//(\muparrow{}isl(d  x  y))
\mvdash{}  A  \msim{}  a:x,y:A//(\mdownarrow{}E[x;y])  \mtimes{}  \{b:A|  \muparrow{}isl(d  a  b)\} 


By

---

Latex:
((Assert  a:x,y:A//(\muparrow{}isl(d  x  y))  \mtimes{}  \{b:A|  \muparrow{}isl(d  a  b)\}    \mmember{}  Type  BY
                (MemCD
                  THEN  Try  (Complete  (Auto))
                  THEN  (Subst'  \{b:A|  \muparrow{}isl(d  a  b)\}    \msim{}  equiv-class(A;a,b.isl(d  a  b);a)  0
                              THENA  (RepUR  ``equiv-class``  0  THEN  Auto)
                              )
                  THEN  Auto))
  THEN  (Assert  a:x,y:A//(\mdownarrow{}E[x;y])  \mtimes{}  \{b:A|  \muparrow{}isl(d  a  b)\}    \mmember{}  Type  BY
                          (MemCD
                            THEN  Try  (Complete  (Auto))
                            THEN  (Subst'  \{b:A|  \muparrow{}isl(d  a  b)\}    \msim{}  equiv-class(A;a,b.isl(d  a  b);a)  0
                                        THENA  (RepUR  ``equiv-class``  0  THEN  Auto)
                                        )
                            THEN  Auto))
  )

---

Home Index