---

Step * 2 of Lemma subset-trans_wf

.....set predicate..... 
1. 𝔽 ∈ small_cubical_set{j:l}
2. I : fset(ℕ)
3. J : fset(ℕ)
4. f : J ⟶ I
5. psi : 𝔽(I)
⊢ ∀A,B:fset(ℕ). ∀g:B ⟶ A.
    ((λx.(λK,g. f ⋅ g) A x ⋅ g) = (λx.((λK,g. f ⋅ g) B x ⋅ g)) ∈ ({f@0:A ⟶ J| ((psi)<f> f@0) = 1}  ⟶ {f:B ⟶ I| (psi f\000C) = 1} ))
BY
{ Auto }

1
1. 𝔽 ∈ small_cubical_set{j:l}
2. I : fset(ℕ)
3. J : fset(ℕ)
4. f : J ⟶ I
5. psi : 𝔽(I)
6. A : fset(ℕ)
7. B : fset(ℕ)
8. g : B ⟶ A
⊢ (λx.f ⋅ x ⋅ g) = (λx.f ⋅ x ⋅ g) ∈ ({f@0:A ⟶ J| ((psi)<f> f@0) = 1}  ⟶ {f:B ⟶ I| (psi f) = 1} )

---

Latex:

---

Latex:
.....set  predicate..... 
1.  \mBbbF{}  \mmember{}  small\_cubical\_set\{j:l\}
2.  I  :  fset(\mBbbN{})
3.  J  :  fset(\mBbbN{})
4.  f  :  J  {}\mrightarrow{}  I
5.  psi  :  \mBbbF{}(I)
\mvdash{}  \mforall{}A,B:fset(\mBbbN{}).  \mforall{}g:B  {}\mrightarrow{}  A.    ((\mlambda{}x.(\mlambda{}K,g.  f  \mcdot{}  g)  A  x  \mcdot{}  g)  =  (\mlambda{}x.((\mlambda{}K,g.  f  \mcdot{}  g)  B  x  \mcdot{}  g)))


By

---

Latex:
Auto

---

Home Index