---

Step * 1 of Lemma cubical-term-subtype-cubical-subset


1. I : fset(ℕ)
2. psi : 𝔽(I)
3. T : {formal-cube(I) ⊢ _}
4. x : I@0:fset(ℕ) ⟶ a:formal-cube(I)(I@0) ⟶ T(a)
5. ∀I@0,J:fset(ℕ). ∀f:J ⟶ I@0. ∀a:formal-cube(I)(I@0).  ((x I@0 a a f) = (x J f(a)) ∈ T(f(a)))
⊢ x ∈ I@0:fset(ℕ) ⟶ a:I,psi(I@0) ⟶ T(a)
BY
{ ((RWO "cubical-subset-I_cube" 0 THENA Auto) THEN RepUR ``formal-cube`` 4 THEN Auto) }

---

Latex:

---

Latex:

1.  I  :  fset(\mBbbN{})
2.  psi  :  \mBbbF{}(I)
3.  T  :  \{formal-cube(I)  \mvdash{}  \_\}
4.  x  :  I@0:fset(\mBbbN{})  {}\mrightarrow{}  a:formal-cube(I)(I@0)  {}\mrightarrow{}  T(a)
5.  \mforall{}I@0,J:fset(\mBbbN{}).  \mforall{}f:J  {}\mrightarrow{}  I@0.  \mforall{}a:formal-cube(I)(I@0).    ((x  I@0  a  a  f)  =  (x  J  f(a)))
\mvdash{}  x  \mmember{}  I@0:fset(\mBbbN{})  {}\mrightarrow{}  a:I,psi(I@0)  {}\mrightarrow{}  T(a)


By

---

Latex:
((RWO  "cubical-subset-I\_cube"  0  THENA  Auto)  THEN  RepUR  ``formal-cube``  4  THEN  Auto)

---

Home Index