---

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

.....subterm..... T:t
2:n
1. I : fset(ℕ)
2. phi : {formal-cube(I) ⊢ _:𝔽}
⊢ (λI@0,J,f,rho. f(rho))
= (λU,U',f,ux. (cat-comp(CubeCat) U' U I f ux))
∈ (x:fset(ℕ)
  ⟶ y:fset(ℕ)
  ⟶ y ⟶ x
  ⟶ ((λI@0.{rho:formal-cube(I)(I@0)| phi(rho) = 1 ∈ Point(face_lattice(I@0))} ) x)
  ⟶ ((λI@0.{rho:formal-cube(I)(I@0)| phi(rho) = 1 ∈ Point(face_lattice(I@0))} ) y))
BY
{ RepUR ``cat-comp cube-cat cat-arrow`` 0 }

1
1. I : fset(ℕ)
2. phi : {formal-cube(I) ⊢ _:𝔽}
⊢ (λI@0,J,f,rho. f(rho))
= (λU,U',f,ux. ux ⋅ f)
∈ (x:fset(ℕ)
  ⟶ y:fset(ℕ)
  ⟶ y ⟶ x
  ⟶ {rho:formal-cube(I)(x)| phi(rho) = 1 ∈ Point(face_lattice(x))} 
  ⟶ {rho:formal-cube(I)(y)| phi(rho) = 1 ∈ Point(face_lattice(y))} )

---

Latex:

---

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


By

---

Latex:
RepUR  ``cat-comp  cube-cat  cat-arrow``  0

---

Home Index