---

Step * 1 of Lemma composition-type-lemma1


1. Gamma : CubicalSet{j}
2. A : {Gamma.𝕀 ⊢ _}
3. I : fset(ℕ)
4. rho : Gamma(I)
⊢ (A)[0(𝕀)](rho) = A((new-name(I)0)((s(rho);<new-name(I)>))) ∈ 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-0`` 0
   THEN (RWO "cc-adjoin-cube-restriction" 0 THENA Auto)
   THEN (Fold `cc-adjoin-cube` 0 THEN EqCD)
   THEN Auto) }

1
.....subterm..... T:t
2:n
1. Gamma : CubicalSet{j}
2. A : {Gamma.𝕀 ⊢ _}
3. I : fset(ℕ)
4. rho : Gamma(I)
⊢ 0 = (<new-name(I)> s(rho) (new-name(I)0)) ∈ 𝕀(rho)

---

Latex:

---

Latex:

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


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-0``  0
  THEN  (RWO  "cc-adjoin-cube-restriction"  0  THENA  Auto)
  THEN  (Fold  `cc-adjoin-cube`  0  THEN  EqCD)
  THEN  Auto)

---

Home Index