---

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


1. I : fset(ℕ)
2. phi : {formal-cube(I) ⊢ _:𝔽}
3. x : fset(ℕ)
⊢ {rho:formal-cube(I)(x)| phi(rho) = 1 ∈ Point(face_lattice(x))}  = {f:cat-arrow(CubeCat) x I| (phi(1) f) = 1}  ∈ 𝕌{j'}
BY
{ RepUR ``cat-arrow names-cat formal-cube cubical-term-at name-morph-satisfies`` 0 }

1
1. I : fset(ℕ)
2. phi : {formal-cube(I) ⊢ _:𝔽}
3. x : fset(ℕ)
⊢ {rho:x ⟶ I| (phi x rho) = 1 ∈ Point(face_lattice(x))} 
= {f:(fst(snd(CubeCat))) x I| (phi I 1)<f> = 1 ∈ Point(face_lattice(x))} 
∈ 𝕌{j'}

---

Latex:

---

Latex:

1.  I  :  fset(\mBbbN{})
2.  phi  :  \{formal-cube(I)  \mvdash{}  \_:\mBbbF{}\}
3.  x  :  fset(\mBbbN{})
\mvdash{}  \{rho:formal-cube(I)(x)|  phi(rho)  =  1\}    =  \{f:cat-arrow(CubeCat)  x  I|  (phi(1)  f)  =  1\} 


By

---

Latex:
RepUR  ``cat-arrow  names-cat  formal-cube  cubical-term-at  name-morph-satisfies``  0

---

Home Index