---

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


1. H : CubicalSet{j}
⊢ [0(𝕀)] o p = m o [0(𝕀)] ∈ H.𝕀 ij⟶ H.𝕀
BY
{ (BLemma `csm-equal2`
   THEN Auto
   THEN RepUR ``cube-context-adjoin`` -1
   THEN D -1
   THEN RepUR ``cube-context-adjoin`` 0
   THEN CsmUnfoldingNotInterval
   THEN EqCDA) }

1
.....subterm..... T:t
2:n
1. H : CubicalSet{j}
2. K : fset(ℕ)
3. alpha : H(K)
4. x1 : 𝕀(alpha)
⊢ 0 = x1 ∧ 0 ∈ 𝕀(alpha)

---

Latex:

---

Latex:

1.  H  :  CubicalSet\{j\}
\mvdash{}  [0(\mBbbI{})]  o  p  =  m  o  [0(\mBbbI{})]


By

---

Latex:
(BLemma  `csm-equal2`
  THEN  Auto
  THEN  RepUR  ``cube-context-adjoin``  -1
  THEN  D  -1
  THEN  RepUR  ``cube-context-adjoin``  0
  THEN  CsmUnfoldingNotInterval
  THEN  EqCDA)

---

Home Index