---

Step * 1 of Lemma quotient-of-quotient


1. T : Type
2. R : T ⟶ T ⟶ ℙ
3. EquivRel(T;x,y.x R y)
4. Q : (x,y:T//(x R y)) ⟶ (x,y:T//(x R y)) ⟶ ℙ
5. EquivRel(x,y:T//(x R y);u,v.u Q v)
6. EquivRel(T;x,y.x Q y)
7. x,y:T//(x Q y) ∈ Type
8. a : x,y:T//(x R y)
9. b : x,y:T//(x R y)
10. a Q b
⊢ a = b ∈ (x,y:T//(x Q y))
BY
{ (DVar `a' THEN DVar `b' THEN EqTypeCD THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  R  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
3.  EquivRel(T;x,y.x  R  y)
4.  Q  :  (x,y:T//(x  R  y))  {}\mrightarrow{}  (x,y:T//(x  R  y))  {}\mrightarrow{}  \mBbbP{}
5.  EquivRel(x,y:T//(x  R  y);u,v.u  Q  v)
6.  EquivRel(T;x,y.x  Q  y)
7.  x,y:T//(x  Q  y)  \mmember{}  Type
8.  a  :  x,y:T//(x  R  y)
9.  b  :  x,y:T//(x  R  y)
10.  a  Q  b
\mvdash{}  a  =  b


By

---

Latex:
(DVar  `a'  THEN  DVar  `b'  THEN  EqTypeCD  THEN  Auto)

---

Home Index