---

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

1
.....assertion..... 
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))
⊢ λx.x ∈ f,g:⇃(Base) ⟶ Base//fun-equiv(⇃(Base);a,b.↓True;f;g)

2
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))
3. λx.x ∈ 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))))
2.  (\00D9(Base)  {}\mrightarrow{}  \00D9(Base))  \msubseteq{}r  (f,g:\00D9(Base)  {}\mrightarrow{}  Base//fun-equiv(\00D9(Base);a,b.\mdownarrow{}True;f;g))
\mvdash{}  False


By

---

Latex:
Assert  \mkleeneopen{}\mlambda{}x.x  \mmember{}  f,g:\00D9(Base)  {}\mrightarrow{}  Base//fun-equiv(\00D9(Base);a,b.\mdownarrow{}True;f;g)\mkleeneclose{}\mcdot{}

---

Home Index