---

Step * of Lemma quotient-of-quotient

∀T:Type. ∀R:T ⟶ T ⟶ ℙ.
  (EquivRel(T;x,y.x R y)
  ⇒ (∀Q:(x,y:T//(x R y)) ⟶ (x,y:T//(x R y)) ⟶ ℙ
        (EquivRel(x,y:T//(x R y);u,v.u Q v) ⇒ u,v:x,y:T//(x R y)//(u Q v) ≡ x,y:T//(x Q y))))
BY
{ ((Auto THEN (Assert EquivRel(T;x,y.x Q y) BY (BLemma `equiv-on-quotient` THEN Auto)))
   THEN (Assert x,y:T//(x Q y) ∈ Type BY
               Auto)
   THEN RepeatFor 2 ((D 0 THEN Auto))
   THEN D -1
   THEN (MoveToConcl (-1) THEN (GenConcl ⌜x = a ∈ (x,y:T//(x R y))⌝⋅ THENA Auto) THEN ThinVar `x')
   THEN (GenConcl ⌜x1 = b ∈ (x,y:T//(x R y))⌝⋅ THENA Auto)
   THEN ThinVar `x1'
   THEN (D 0 THENA Auto)) }

1
1. T : Type
2. R : T ⟶ T ⟶ ℙ
3. EquivRel(T;x,y.x R y)
4. Q : (x,y:T//(x R y)) ⟶ (x,y:T//(x R y)) ⟶ ℙ
5. EquivRel(x,y:T//(x R y);u,v.u Q v)
6. EquivRel(T;x,y.x Q y)
7. x,y:T//(x Q y) ∈ Type
8. a : x,y:T//(x R y)
9. b : x,y:T//(x R y)
10. a Q b
⊢ a = b ∈ (x,y:T//(x Q y))

---

Latex:

---

Latex:
\mforall{}T:Type.  \mforall{}R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}.
    (EquivRel(T;x,y.x  R  y)
    {}\mRightarrow{}  (\mforall{}Q:(x,y:T//(x  R  y))  {}\mrightarrow{}  (x,y:T//(x  R  y))  {}\mrightarrow{}  \mBbbP{}
                (EquivRel(x,y:T//(x  R  y);u,v.u  Q  v)  {}\mRightarrow{}  u,v:x,y:T//(x  R  y)//(u  Q  v)  \mequiv{}  x,y:T//(x  Q  y))))


By

---

Latex:
((Auto  THEN  (Assert  EquivRel(T;x,y.x  Q  y)  BY  (BLemma  `equiv-on-quotient`  THEN  Auto)))
  THEN  (Assert  x,y:T//(x  Q  y)  \mmember{}  Type  BY
                          Auto)
  THEN  RepeatFor  2  ((D  0  THEN  Auto))
  THEN  D  -1
  THEN  (MoveToConcl  (-1)  THEN  (GenConcl  \mkleeneopen{}x  =  a\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  ThinVar  `x')
  THEN  (GenConcl  \mkleeneopen{}x1  =  b\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  ThinVar  `x1'
  THEN  (D  0  THENA  Auto))

---

Home Index