---

Step * 2 of Lemma cubical-subset-is-context-subset

.....wf..... 
1. I : fset(ℕ)
2. psi : 𝔽(I)
3. formal-cube(I) j⊢
4. ∀[X,Y:j⊢].
     X = Y ∈ CubicalSet{j} supposing X = Y ∈ (F:fset(ℕ) ⟶ 𝕌{j'} × (x:fset(ℕ) ⟶ y:fset(ℕ) ⟶ y ⟶ x ⟶ (F x) ⟶ (F y)))
⊢ formal-cube(I), λJ,f. f(psi) j⊢
BY
{ Auto }

1
1. I : fset(ℕ)
2. psi : 𝔽(I)
3. formal-cube(I) j⊢
4. ∀[X,Y:j⊢].
     X = Y ∈ CubicalSet{j} supposing X = Y ∈ (F:fset(ℕ) ⟶ 𝕌{j'} × (x:fset(ℕ) ⟶ y:fset(ℕ) ⟶ y ⟶ x ⟶ (F x) ⟶ (F y)))
⊢ λJ,f. f(psi) ∈ {formal-cube(I) ⊢ _:𝔽}

---

Latex:

---

Latex:
.....wf..... 
1.  I  :  fset(\mBbbN{})
2.  psi  :  \mBbbF{}(I)
3.  formal-cube(I)  j\mvdash{}
4.  \mforall{}[X,Y:j\mvdash{}].    X  =  Y  supposing  X  =  Y
\mvdash{}  formal-cube(I),  \mlambda{}J,f.  f(psi)  j\mvdash{}


By

---

Latex:
Auto

---

Home Index