---

Step * of Lemma not-quotient-function-subtype

¬(∀[X,A:Type]. ∀[E:A ⟶ A ⟶ ℙ].
    (EquivRel(A;a,b.E[a;b]) ⇒ ((X ⟶ (a,b:A//E[a;b])) ⊆r (f,g:X ⟶ A//fun-equiv(X;a,b.↓E[a;b];f;g)))))
BY
{ (D 0 THENA Auto) }

1
1. ∀[X,A:Type]. ∀[E:A ⟶ A ⟶ ℙ].
     (EquivRel(A;a,b.E[a;b]) ⇒ ((X ⟶ (a,b:A//E[a;b])) ⊆r (f,g:X ⟶ A//fun-equiv(X;a,b.↓E[a;b];f;g))))
⊢ False

2
1. X : Type
2. A : Type
3. E : A ⟶ A ⟶ ℙ
4. x : EquivRel(A;a,b.E[a;b])
⊢ EquivRel(X ⟶ A;f,g.fun-equiv(X;a,b.↓E[a;b];f;g))

---

Latex:

---

Latex:
\mneg{}(\mforall{}[X,A:Type].  \mforall{}[E:A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}].
        (EquivRel(A;a,b.E[a;b])
        {}\mRightarrow{}  ((X  {}\mrightarrow{}  (a,b:A//E[a;b]))  \msubseteq{}r  (f,g:X  {}\mrightarrow{}  A//fun-equiv(X;a,b.\mdownarrow{}E[a;b];f;g)))))


By

---

Latex:
(D  0  THENA  Auto)

---

Home Index