---

Step * 1 1 of Lemma context-subset-term-1


1. Gamma : CubicalSet{j}
2. T : {Gamma ⊢ _}
3. x : I:fset(ℕ) ⟶ a:Gamma(I) ⟶ T(a)
4. ∀I,J:fset(ℕ). ∀f:J ⟶ I. ∀a:Gamma(I).  ((x I a a f) = (x J f(a)) ∈ T(f(a)))
⊢ x ∈ {Gamma, 1(𝔽) ⊢ _:T}
BY
{ RepUR ``cubical-term context-subset`` 0 }

1
1. Gamma : CubicalSet{j}
2. T : {Gamma ⊢ _}
3. x : I:fset(ℕ) ⟶ a:Gamma(I) ⟶ T(a)
4. ∀I,J:fset(ℕ). ∀f:J ⟶ I. ∀a:Gamma(I).  ((x I a a f) = (x J f(a)) ∈ T(f(a)))
⊢ x ∈ {u:I:fset(ℕ) ⟶ a:{rho:Gamma(I)| 1(𝔽)(rho) = 1 ∈ Point(face_lattice(I))}  ⟶ T(a)| 
       ∀I,J:fset(ℕ). ∀f:J ⟶ I. ∀a:{rho:Gamma(I)| 1(𝔽)(rho) = 1 ∈ Point(face_lattice(I))} .
         ((u I a a f) = (u J f(a)) ∈ T(f(a)))} 

---

Latex:

---

Latex:

1.  Gamma  :  CubicalSet\{j\}
2.  T  :  \{Gamma  \mvdash{}  \_\}
3.  x  :  I:fset(\mBbbN{})  {}\mrightarrow{}  a:Gamma(I)  {}\mrightarrow{}  T(a)
4.  \mforall{}I,J:fset(\mBbbN{}).  \mforall{}f:J  {}\mrightarrow{}  I.  \mforall{}a:Gamma(I).    ((x  I  a  a  f)  =  (x  J  f(a)))
\mvdash{}  x  \mmember{}  \{Gamma,  1(\mBbbF{})  \mvdash{}  \_:T\}


By

---

Latex:
RepUR  ``cubical-term  context-subset``  0

---

Home Index