---

Step * 1 1 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
13. y ∈ X
14. E1[x;y]
15. x = x ∈ (x,y:T//E2[x;y])
16. x ∈ T
17. x ∈ T
18. E2[x;x]
⊢ x = y ∈ (x,y:T//E2[x;y])
BY
{ ((InstHyp [⌜x⌝;⌜y⌝] 8⋅ THENA Auto) THEN D -1) }

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 ∈ (x,y:T//E2[x;y])
16. x ∈ T
17. x ∈ T
18. E2[x;x]
19. y ∈ T
20. 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
13.  y  \mmember{}  X
14.  E1[x;y]
15.  x  =  x
16.  x  \mmember{}  T
17.  x  \mmember{}  T
18.  E2[x;x]
\mvdash{}  x  =  y


By

---

Latex:
((InstHyp  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{}]  8\mcdot{}  THENA  Auto)  THEN  D  -1)

---

Home Index