---

Step * 1 of Lemma composition-type-lemma2


1. Gamma : CubicalSet{j}
2. A : {Gamma.𝕀 ⊢ _}
3. I : fset(ℕ)
4. rho : Gamma(I)
⊢ A((new-name(I)1)((s(rho);<new-name(I)>))) = (A)[1(𝕀)](rho) ∈ Type
BY
{ ((RWO "csm-ap-type-at" 0 THENA Auto)
   THEN EqCD
   THEN Auto
   THEN RepUR ``csm-ap csm-id-adjoin csm-adjoin csm-id interval-1`` 0
   THEN (RWO "cc-adjoin-cube-restriction" 0 THENA Auto)
   THEN (Fold `cc-adjoin-cube` 0 THEN EqCD)
   THEN Auto) }

---

Latex:

---

Latex:

1.  Gamma  :  CubicalSet\{j\}
2.  A  :  \{Gamma.\mBbbI{}  \mvdash{}  \_\}
3.  I  :  fset(\mBbbN{})
4.  rho  :  Gamma(I)
\mvdash{}  A((new-name(I)1)((s(rho);<new-name(I)>)))  =  (A)[1(\mBbbI{})](rho)


By

---

Latex:
((RWO  "csm-ap-type-at"  0  THENA  Auto)
  THEN  EqCD
  THEN  Auto
  THEN  RepUR  ``csm-ap  csm-id-adjoin  csm-adjoin  csm-id  interval-1``  0
  THEN  (RWO  "cc-adjoin-cube-restriction"  0  THENA  Auto)
  THEN  (Fold  `cc-adjoin-cube`  0  THEN  EqCD)
  THEN  Auto)

---

Home Index