---

Step * 1 of Lemma respects-equality-quotient


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])
BY
{ (EqTypeHD (-2) THENA 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
13. y ∈ X
14. E1[x;y]
15. x ∈ x,y:T//E2[x;y]
⊢ x = y ∈ (x,y:T//E2[x;y])

---

Latex:

---

Latex:

1.  X  :  Type
2.  T  :  Type
3.  E1  :  X  {}\mrightarrow{}  X  {}\mrightarrow{}  \mBbbP{}
4.  E2  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
5.  EquivRel(T;x,y.E2[x;y])
6.  EquivRel(X;x,y.E1[x;y])
7.  respects-equality(X;T)
8.  \mforall{}x,y:X.    (E1[x;y]  {}\mRightarrow{}  (x  \mmember{}  T)  {}\mRightarrow{}  ((y  \mmember{}  T)  \mwedge{}  E2[x;y]))
9.  x  :  Base
10.  y  :  Base
11.  x  =  y
12.  x  \mmember{}  x,y:T//E2[x;y]
\mvdash{}  x  =  y


By

---

Latex:
(EqTypeHD  (-2)  THENA  Auto)

---

Home Index