---

Step * 1 1 of Lemma face-zero-eq-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))
BY
{ Auto }

---

Latex:

---

Latex:
.....fun  wf..... 
1.  H  :  CubicalSet\{j\}
2.  z  :  \{H  \mvdash{}  \_:\mBbbI{}\}
3.  I  :  fset(\mBbbN{})
4.  a  :  H(I)
5.  \mneg{}(z(a))  =  1
6.  Z  :  Point(dM(I))
\mvdash{}  \mneg{}(Z)  =  \mneg{}(Z)


By

---

Latex:
Auto

---

Home Index