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


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

1
1. Gamma CubicalSet{j}
2. {Gamma ⊢ _}
3. I:fset(ℕ) ⟶ a:Gamma(I) ⟶ T(a)
4. ∀I,J:fset(ℕ). ∀f:J ⟶ I. ∀a:Gamma(I).  ((x f) (x 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 f) (u 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