---

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

.....subterm..... T:t
1:n
1. Gamma : CubicalSet{j}
2. T : {Gamma ⊢ _}
3. x : Top
⊢ x ∈ {Gamma, 0(𝔽) ⊢ _:T}
BY
{ ((Unfold `cubical-term` 0 THEN At ⌜𝕌'⌝ MemTypeCD⋅)
   THEN RepUR ``context-subset face-0 cubical-term-at`` 0
   THEN Intros) }

1
1. Gamma : CubicalSet{j}
2. T : {Gamma ⊢ _}
3. x : Top
⊢ x ∈ I:fset(ℕ) ⟶ a:{rho:Gamma(I)| 0 = 1 ∈ Point(face_lattice(I))}  ⟶ T(a)

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

3
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))))

---

Latex:

---

Latex:
.....subterm.....  T:t
1:n
1.  Gamma  :  CubicalSet\{j\}
2.  T  :  \{Gamma  \mvdash{}  \_\}
3.  x  :  Top
\mvdash{}  x  \mmember{}  \{Gamma,  0(\mBbbF{})  \mvdash{}  \_:T\}


By

---

Latex:
((Unfold  `cubical-term`  0  THEN  At  \mkleeneopen{}\mBbbU{}'\mkleeneclose{}  MemTypeCD\mcdot{})
  THEN  RepUR  ``context-subset  face-0  cubical-term-at``  0
  THEN  Intros)

---

Home Index