---

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


1. Gamma : CubicalSet{j}
2. T : {Gamma ⊢ _}
3. x : Top
4. u : I:fset(ℕ) ⟶ a:Gamma, 0(𝔽)(I) ⟶ T(a)
⊢ istype(∀I,J:fset(ℕ). ∀f:J ⟶ I. ∀a:{rho:Gamma(I)| 0 = 1 ∈ Point(face_lattice(I))} .
           ((u I a a f) = (u J f(a)) ∈ T(f(a))))
BY
{ RepeatFor 4 ((D 0 THENL [Auto; Id])) }

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

---

Latex:

---

Latex:

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


By

---

Latex:
RepeatFor  4  ((D  0  THENL  [Auto;  Id]))

---

Home Index