---

Step * 2 of Lemma discrete-map-is-constant2

.....wf..... 
1. T : Type
2. I : fset(ℕ)
3. phi : 𝔽(I)
4. s : A:fset(ℕ) ⟶ {f:A ⟶ I| (phi f) = 1}  ⟶ T
5. ∀A,B:fset(ℕ). ∀g:B ⟶ A.  ((λx.(s A x)) = (λx.(s B x ⋅ g)) ∈ ({f:A ⟶ I| (phi f) = 1}  ⟶ T))
6. f : {f:I ⟶ I| (phi f) = 1} 
7. ∀[J:fset(ℕ)]. ∀[g:J ⟶ I].  ((phi g) = 1 ⇒ (g = f ⋅ g ∈ J ⟶ I))
8. trans : A:fset(ℕ) ⟶ {f:A ⟶ I| (phi f) = 1}  ⟶ T
⊢ istype(∀A,B:fset(ℕ). ∀g:B ⟶ A.  ((λx.(trans A x)) = (λx.(trans B x ⋅ g)) ∈ ({f:A ⟶ I| (phi f) = 1}  ⟶ T)))
BY
{ Assert ⌜∀A,B:fset(ℕ). ∀g:B ⟶ A. ∀x:{f:A ⟶ I| (phi f) = 1} .  (x ⋅ g ∈ {f:B ⟶ I| (phi f) = 1} )⌝⋅ }

1
.....assertion..... 
1. T : Type
2. I : fset(ℕ)
3. phi : 𝔽(I)
4. s : A:fset(ℕ) ⟶ {f:A ⟶ I| (phi f) = 1}  ⟶ T
5. ∀A,B:fset(ℕ). ∀g:B ⟶ A.  ((λx.(s A x)) = (λx.(s B x ⋅ g)) ∈ ({f:A ⟶ I| (phi f) = 1}  ⟶ T))
6. f : {f:I ⟶ I| (phi f) = 1} 
7. ∀[J:fset(ℕ)]. ∀[g:J ⟶ I].  ((phi g) = 1 ⇒ (g = f ⋅ g ∈ J ⟶ I))
8. trans : A:fset(ℕ) ⟶ {f:A ⟶ I| (phi f) = 1}  ⟶ T
⊢ ∀A,B:fset(ℕ). ∀g:B ⟶ A. ∀x:{f:A ⟶ I| (phi f) = 1} .  (x ⋅ g ∈ {f:B ⟶ I| (phi f) = 1} )

2
1. T : Type
2. I : fset(ℕ)
3. phi : 𝔽(I)
4. s : A:fset(ℕ) ⟶ {f:A ⟶ I| (phi f) = 1}  ⟶ T
5. ∀A,B:fset(ℕ). ∀g:B ⟶ A.  ((λx.(s A x)) = (λx.(s B x ⋅ g)) ∈ ({f:A ⟶ I| (phi f) = 1}  ⟶ T))
6. f : {f:I ⟶ I| (phi f) = 1} 
7. ∀[J:fset(ℕ)]. ∀[g:J ⟶ I].  ((phi g) = 1 ⇒ (g = f ⋅ g ∈ J ⟶ I))
8. trans : A:fset(ℕ) ⟶ {f:A ⟶ I| (phi f) = 1}  ⟶ T
9. ∀A,B:fset(ℕ). ∀g:B ⟶ A. ∀x:{f:A ⟶ I| (phi f) = 1} .  (x ⋅ g ∈ {f:B ⟶ I| (phi f) = 1} )
⊢ istype(∀A,B:fset(ℕ). ∀g:B ⟶ A.  ((λx.(trans A x)) = (λx.(trans B x ⋅ g)) ∈ ({f:A ⟶ I| (phi f) = 1}  ⟶ T)))

---

Latex:

---

Latex:
.....wf..... 
1.  T  :  Type
2.  I  :  fset(\mBbbN{})
3.  phi  :  \mBbbF{}(I)
4.  s  :  A:fset(\mBbbN{})  {}\mrightarrow{}  \{f:A  {}\mrightarrow{}  I|  (phi  f)  =  1\}    {}\mrightarrow{}  T
5.  \mforall{}A,B:fset(\mBbbN{}).  \mforall{}g:B  {}\mrightarrow{}  A.    ((\mlambda{}x.(s  A  x))  =  (\mlambda{}x.(s  B  x  \mcdot{}  g)))
6.  f  :  \{f:I  {}\mrightarrow{}  I|  (phi  f)  =  1\} 
7.  \mforall{}[J:fset(\mBbbN{})].  \mforall{}[g:J  {}\mrightarrow{}  I].    ((phi  g)  =  1  {}\mRightarrow{}  (g  =  f  \mcdot{}  g))
8.  trans  :  A:fset(\mBbbN{})  {}\mrightarrow{}  \{f:A  {}\mrightarrow{}  I|  (phi  f)  =  1\}    {}\mrightarrow{}  T
\mvdash{}  istype(\mforall{}A,B:fset(\mBbbN{}).  \mforall{}g:B  {}\mrightarrow{}  A.    ((\mlambda{}x.(trans  A  x))  =  (\mlambda{}x.(trans  B  x  \mcdot{}  g))))


By

---

Latex:
Assert  \mkleeneopen{}\mforall{}A,B:fset(\mBbbN{}).  \mforall{}g:B  {}\mrightarrow{}  A.  \mforall{}x:\{f:A  {}\mrightarrow{}  I|  (phi  f)  =  1\}  .    (x  \mcdot{}  g  \mmember{}  \{f:B  {}\mrightarrow{}  I|  (phi  f)  =  1\}  )\mkleeneclose{}\mcdot{}

---

Home Index