---

Step * 1 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.𝕀(I)
7. (q=0)(a) = 1 ∈ Point(face_lattice(I))
⊢ (z I a) = (((z)[0(𝕀)])p I a) ∈ (B)p(a)
BY
{ (InstLemma `face-zero-eq-1` [⌜Gamma.𝕀⌝;⌜q⌝;⌜I⌝;⌜a⌝]⋅ THENA Auto) }

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))
8. q(a) = 0 ∈ 𝕀(a)
⊢ (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{}(I)
7.  (q=0)(a)  =  1
\mvdash{}  (z  I  a)  =  (((z)[0(\mBbbI{})])p  I  a)


By

---

Latex:
(InstLemma  `face-zero-eq-1`  [\mkleeneopen{}Gamma.\mBbbI{}\mkleeneclose{};\mkleeneopen{}q\mkleeneclose{};\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{}]\mcdot{}  THENA  Auto)

---

Home Index