---

Step * 1 of Lemma quotient-member-eq


1. T : Type
2. E : T ⟶ T ⟶ ℙ
3. EquivRel(T;x,y.E[x;y])
4. x : T
5. y : T
6. E[x;y]
⊢ x = y ∈ (x,y:T//E[x;y])
BY
{ (PointwiseFunctionality 4
   THEN PointwiseFunctionality 7
   THEN Repeat ((EqCD THEN Auto))
   THEN At ⌜Type⌝ PerEqCD⋅
   THEN Try (Fold `quotient` 0⋅)
   THEN Reduce 0
   THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  T  :  Type
2.  E  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
3.  EquivRel(T;x,y.E[x;y])
4.  x  :  T
5.  y  :  T
6.  E[x;y]
\mvdash{}  x  =  y


By

---

Latex:
(PointwiseFunctionality  4
  THEN  PointwiseFunctionality  7
  THEN  Repeat  ((EqCD  THEN  Auto))
  THEN  At  \mkleeneopen{}Type\mkleeneclose{}  PerEqCD\mcdot{}
  THEN  Try  (Fold  `quotient`  0\mcdot{})
  THEN  Reduce  0
  THEN  Auto)\mcdot{}

---

Home Index