---

Step * of Lemma quo-lift_wf

∀A,B:Type. ∀f:A ⟶ B. ∀R:B ⟶ B ⟶ ℙ.  (EquivRel(B;x,y.x R y) ⇒ (quo-lift(f) ∈ (x,y:A//(x R_f y)) ⟶ (x,y:B//(x R y))))
BY
{ (Auto
   THEN (Assert EquivRel(A;x,y.x R_f y) BY
               (BLemma `preima_of_equiv_rel` THEN Auto))
   THEN (FunExt THENA Auto)
   THEN D -1) }

1
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))

---

Latex:

---

Latex:
\mforall{}A,B:Type.  \mforall{}f:A  {}\mrightarrow{}  B.  \mforall{}R:B  {}\mrightarrow{}  B  {}\mrightarrow{}  \mBbbP{}.
    (EquivRel(B;x,y.x  R  y)  {}\mRightarrow{}  (quo-lift(f)  \mmember{}  (x,y:A//(x  R\_f  y))  {}\mrightarrow{}  (x,y:B//(x  R  y))))


By

---

Latex:
(Auto
  THEN  (Assert  EquivRel(A;x,y.x  R\_f  y)  BY
                          (BLemma  `preima\_of\_equiv\_rel`  THEN  Auto))
  THEN  (FunExt  THENA  Auto)
  THEN  D  -1)

---

Home Index