---

Step * 1 of Lemma quo-lift_wf


1. A : Type
2. B : Type
3. f : A ⟶ B
4. R : B ⟶ B ⟶ ℙ
5. EquivRel(B;x,y.x R y)
6. EquivRel(A;x,y.x R_f y)
7. x : Base
8. x1 : Base
9. x = x1 ∈ pertype(λx,y. ((x ∈ A) ∧ (y ∈ A) ∧ (x R_f y)))
10. x ∈ A
11. x1 ∈ A
12. x R_f x1
⊢ (quo-lift(f) x) = (quo-lift(f) x1) ∈ (x,y:B//(x R y))
BY
{ (RepUR ``preima_of_rel`` -1 THEN RepUR ``quo-lift`` 0 THEN EqTypeCD THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  f  :  A  {}\mrightarrow{}  B
4.  R  :  B  {}\mrightarrow{}  B  {}\mrightarrow{}  \mBbbP{}
5.  EquivRel(B;x,y.x  R  y)
6.  EquivRel(A;x,y.x  R\_f  y)
7.  x  :  Base
8.  x1  :  Base
9.  x  =  x1
10.  x  \mmember{}  A
11.  x1  \mmember{}  A
12.  x  R\_f  x1
\mvdash{}  (quo-lift(f)  x)  =  (quo-lift(f)  x1)


By

---

Latex:
(RepUR  ``preima\_of\_rel``  -1  THEN  RepUR  ``quo-lift``  0  THEN  EqTypeCD  THEN  Auto)

---

Home Index