---

Step * 1 1 of Lemma csm-m-comp-0

.....subterm..... T:t
2:n
1. H : CubicalSet{j}
2. K : fset(ℕ)
3. alpha : H(K)
4. x1 : 𝕀(alpha)
⊢ 0 = x1 ∧ 0 ∈ 𝕀(alpha)
BY
{ ((All (RWO "interval-type-at") THENA Auto) THEN All (RepUR  ``interval-presheaf``)) }

1
1. H : CubicalSet{j}
2. K : fset(ℕ)
3. alpha : H(K)
4. x1 : Point(dM(K))
⊢ 0 = x1 ∧ 0 ∈ Point(dM(K))

---

Latex:

---

Latex:
.....subterm.....  T:t
2:n
1.  H  :  CubicalSet\{j\}
2.  K  :  fset(\mBbbN{})
3.  alpha  :  H(K)
4.  x1  :  \mBbbI{}(alpha)
\mvdash{}  0  =  x1  \mwedge{}  0


By

---

Latex:
((All  (RWO  "interval-type-at")  THENA  Auto)  THEN  All  (RepUR    ``interval-presheaf``))

---

Home Index