---

Step * 1 of Lemma not-quotient-function-subtype


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
BY
{ (InstHyp [⌜⇃(Base)⌝;⌜Base⌝;⌜λ2x y.True⌝] 1⋅ 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))))
2. (⇃(Base) ⟶ ⇃(Base)) ⊆r (f,g:⇃(Base) ⟶ Base//fun-equiv(⇃(Base);a,b.↓True;f;g))
⊢ False

---

Latex:

---

Latex:

1.  \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))))
\mvdash{}  False


By

---

Latex:
(InstHyp  [\mkleeneopen{}\00D9(Base)\mkleeneclose{};\mkleeneopen{}Base\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x  y.True\mkleeneclose{}]  1\mcdot{}  THENA  Auto)

---

Home Index