---

Step * 1 of Lemma cubical-term-0-q0


1. Gamma : CubicalSet{j}
2. B : {Gamma ⊢ _}
3. z : {Gamma.𝕀 ⊢ _:(B)p}
4. Gamma.𝕀, (q=0) ⊢ (B)p
5. I : fset(ℕ)
6. a : Gamma.𝕀, (q=0)(I)
⊢ (z I a) = (((z)[0(𝕀)])p I a) ∈ (B)p(a)
BY
{ (RepUR ``context-subset`` -1 THEN D -1) }

1
1. Gamma : CubicalSet{j}
2. B : {Gamma ⊢ _}
3. z : {Gamma.𝕀 ⊢ _:(B)p}
4. Gamma.𝕀, (q=0) ⊢ (B)p
5. I : fset(ℕ)
6. a : Gamma.𝕀(I)
7. (q=0)(a) = 1 ∈ Point(face_lattice(I))
⊢ (z I a) = (((z)[0(𝕀)])p I a) ∈ (B)p(a)

---

Latex:

---

Latex:

1.  Gamma  :  CubicalSet\{j\}
2.  B  :  \{Gamma  \mvdash{}  \_\}
3.  z  :  \{Gamma.\mBbbI{}  \mvdash{}  \_:(B)p\}
4.  Gamma.\mBbbI{},  (q=0)  \mvdash{}  (B)p
5.  I  :  fset(\mBbbN{})
6.  a  :  Gamma.\mBbbI{},  (q=0)(I)
\mvdash{}  (z  I  a)  =  (((z)[0(\mBbbI{})])p  I  a)


By

---

Latex:
(RepUR  ``context-subset``  -1  THEN  D  -1)

---

Home Index