---

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

.....subterm..... T:t
1:n
1. I : fset(ℕ)
2. phi : {formal-cube(I) ⊢ _:𝔽}
⊢ (λI@0.{rho:formal-cube(I)(I@0)| phi(rho) = 1 ∈ Point(face_lattice(I@0))} )
= (λU.{f:cat-arrow(CubeCat) U I| (phi(1) f) = 1} )
∈ (fset(ℕ) ⟶ 𝕌{j'})
BY
{ (FunExt THEN Reduce 0) }

1
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'}

2
.....wf..... 
1. I : fset(ℕ)
2. phi : {formal-cube(I) ⊢ _:𝔽}
⊢ fset(ℕ) ∈ Type

---

Latex:

---

Latex:
.....subterm.....  T:t
1:n
1.  I  :  fset(\mBbbN{})
2.  phi  :  \{formal-cube(I)  \mvdash{}  \_:\mBbbF{}\}
\mvdash{}  (\mlambda{}I@0.\{rho:formal-cube(I)(I@0)|  phi(rho)  =  1\}  )  =  (\mlambda{}U.\{f:cat-arrow(CubeCat)  U  I|  (phi(1)  f)  =  1\}  )


By

---

Latex:
(FunExt  THEN  Reduce  0)

---

Home Index