---

Step * of Lemma respects-equality-quotient

∀[X,T:Type]. ∀[E1:X ⟶ X ⟶ ℙ]. ∀[E2:T ⟶ T ⟶ ℙ].
  (respects-equality(x,y:X//E1[x;y];x,y:T//E2[x;y])) supposing 
     ((∀x,y:X.  (E1[x;y] ⇒ (x ∈ T) ⇒ ((y ∈ T) ∧ E2[x;y]))) and 
     respects-equality(X;T) and 
     EquivRel(X;x,y.E1[x;y]) and 
     EquivRel(T;x,y.E2[x;y]))
BY
{ (Intros THEN (Unhide THENA Auto) THEN RepeatFor 4 ((D 0 THENW Auto))) }

1
1. X : Type
2. T : Type
3. E1 : X ⟶ X ⟶ ℙ
4. E2 : T ⟶ T ⟶ ℙ
5. EquivRel(T;x,y.E2[x;y])
6. EquivRel(X;x,y.E1[x;y])
7. respects-equality(X;T)
8. ∀x,y:X.  (E1[x;y] ⇒ (x ∈ T) ⇒ ((y ∈ T) ∧ E2[x;y]))
9. x : Base
10. y : Base
11. x = y ∈ (x,y:X//E1[x;y])
12. x ∈ x,y:T//E2[x;y]
⊢ x = y ∈ (x,y:T//E2[x;y])

---

Latex:

---

Latex:
\mforall{}[X,T:Type].  \mforall{}[E1:X  {}\mrightarrow{}  X  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[E2:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].
    (respects-equality(x,y:X//E1[x;y];x,y:T//E2[x;y]))  supposing 
          ((\mforall{}x,y:X.    (E1[x;y]  {}\mRightarrow{}  (x  \mmember{}  T)  {}\mRightarrow{}  ((y  \mmember{}  T)  \mwedge{}  E2[x;y])))  and 
          respects-equality(X;T)  and 
          EquivRel(X;x,y.E1[x;y])  and 
          EquivRel(T;x,y.E2[x;y]))


By

---

Latex:
(Intros  THEN  (Unhide  THENA  Auto)  THEN  RepeatFor  4  ((D  0  THENW  Auto)))

---

Home Index