---

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

.....subterm..... T:t
1:n
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)))
⊢ (λU.{f:U ⟶ I| (psi f) = 1} )
= (λI@0.{rho:formal-cube(I)(I@0)| λJ,f. f(psi)(rho) = 1 ∈ Point(face_lattice(I@0))} )
∈ (fset(ℕ) ⟶ 𝕌{j'})
BY
{ (FunExt THEN Reduce 0) }

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)))
5. x : fset(ℕ)
⊢ {f:x ⟶ I| (psi f) = 1}  = {rho:formal-cube(I)(x)| λJ,f. f(psi)(rho) = 1 ∈ Point(face_lattice(x))}  ∈ 𝕌{j'}

2
.....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)))
⊢ fset(ℕ) ∈ Type

---

Latex:

---

Latex:
.....subterm.....  T:t
1:n
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{}  (\mlambda{}U.\{f:U  {}\mrightarrow{}  I|  (psi  f)  =  1\}  )  =  (\mlambda{}I@0.\{rho:formal-cube(I)(I@0)|  \mlambda{}J,f.  f(psi)(rho)  =  1\}  )


By

---

Latex:
(FunExt  THEN  Reduce  0)

---

Home Index