---

Step * 1 of Lemma face-zero-eq-1


1. H : CubicalSet{j}
2. z : {H ⊢ _:𝕀}
3. I : fset(ℕ)
4. a : H(I)
5. ¬(z(a)) = 1 ∈ Point(dM(I))
⊢ z(a) = 0 ∈ 𝕀(a)
BY
{ ApFunToHypEquands `Z' ⌜¬(Z)⌝ ⌜Point(dM(I))⌝ (-1)⋅ }

1
.....fun wf..... 
1. H : CubicalSet{j}
2. z : {H ⊢ _:𝕀}
3. I : fset(ℕ)
4. a : H(I)
5. ¬(z(a)) = 1 ∈ Point(dM(I))
6. Z : Point(dM(I))
⊢ ¬(Z) = ¬(Z) ∈ Point(dM(I))

2
1. H : CubicalSet{j}
2. z : {H ⊢ _:𝕀}
3. I : fset(ℕ)
4. a : H(I)
5. ¬(z(a)) = 1 ∈ Point(dM(I))
6. ¬(¬(z(a))) = ¬(1) ∈ Point(dM(I))
⊢ z(a) = 0 ∈ 𝕀(a)

---

Latex:

---

Latex:

1.  H  :  CubicalSet\{j\}
2.  z  :  \{H  \mvdash{}  \_:\mBbbI{}\}
3.  I  :  fset(\mBbbN{})
4.  a  :  H(I)
5.  \mneg{}(z(a))  =  1
\mvdash{}  z(a)  =  0


By

---

Latex:
ApFunToHypEquands  `Z'  \mkleeneopen{}\mneg{}(Z)\mkleeneclose{}  \mkleeneopen{}Point(dM(I))\mkleeneclose{}  (-1)\mcdot{}

---

Home Index