---

Step * 1 of Lemma subset-trans_wf


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

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

---

Latex:

---

Latex:

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{}  \mlambda{}K,g.  f  \mcdot{}  g  \mmember{}  A:fset(\mBbbN{})  {}\mrightarrow{}  \{f@0:A  {}\mrightarrow{}  J|  ((psi)<f>  f@0)  =  1\}    {}\mrightarrow{}  \{f:A  {}\mrightarrow{}  I|  (psi  f)  =  1\} 


By

---

Latex:
Auto

---

Home Index