---

Step * 1 2 of Lemma cc-fst-comp-csm-m-term


1. H : CubicalSet{j}
2. phi : {H ⊢ _:𝔽}
3. I : fset(ℕ)
4. a : H.𝕀.𝕀(I)
⊢ (((phi)p)m I a) = (((phi)p)p I a) ∈ 𝔽(a)
BY
{ (RepUR ``cube-context-adjoin`` -1 THEN D -1 THEN D -2) }

1
1. H : CubicalSet{j}
2. phi : {H ⊢ _:𝔽}
3. I : fset(ℕ)
4. a2 : H(I)
5. a3 : 𝕀(a2)
6. a1 : 𝕀(<a2, a3>)
⊢ (((phi)p)m I <<a2, a3>, a1>) = (((phi)p)p I <<a2, a3>, a1>) ∈ 𝔽(<<a2, a3>, a1>)

---

Latex:

---

Latex:

1.  H  :  CubicalSet\{j\}
2.  phi  :  \{H  \mvdash{}  \_:\mBbbF{}\}
3.  I  :  fset(\mBbbN{})
4.  a  :  H.\mBbbI{}.\mBbbI{}(I)
\mvdash{}  (((phi)p)m  I  a)  =  (((phi)p)p  I  a)


By

---

Latex:
(RepUR  ``cube-context-adjoin``  -1  THEN  D  -1  THEN  D  -2)

---

Home Index