---

Step * 1 1 of Lemma context-map-cube+-csm+


1. Gamma : CubicalSet{j}
2. I : fset(ℕ)
3. J : fset(ℕ)
4. i : {i:ℕ| ¬i ∈ I} 
5. j : {j:ℕ| ¬j ∈ J} 
6. g : J ⟶ I
7. rho : Gamma(I+i)
8. ∀[A,B:j⊢]. ∀[f:A j⟶ B]. ∀[g:I:fset(ℕ) ⟶ A(I) ⟶ B(I)].
     f = g ∈ A j⟶ B supposing f = g ∈ (I:fset(ℕ) ⟶ A(I) ⟶ B(I))
9. K : fset(ℕ)
10. x : formal-cube(J).𝕀(K)
⊢ (<g,i=j(rho)> o cube+(J;j) K x) = (<rho> o cube+(I;i) o <g>+ K x) ∈ Gamma(K)
BY
{ (RepUR ``formal-cube cube-context-adjoin`` -1 THEN D -1) }

1
1. Gamma : CubicalSet{j}
2. I : fset(ℕ)
3. J : fset(ℕ)
4. i : {i:ℕ| ¬i ∈ I} 
5. j : {j:ℕ| ¬j ∈ J} 
6. g : J ⟶ I
7. rho : Gamma(I+i)
8. ∀[A,B:j⊢]. ∀[f:A j⟶ B]. ∀[g:I:fset(ℕ) ⟶ A(I) ⟶ B(I)].
     f = g ∈ A j⟶ B supposing f = g ∈ (I:fset(ℕ) ⟶ A(I) ⟶ B(I))
9. K : fset(ℕ)
10. alpha : K ⟶ J
11. x1 : 𝕀(alpha)
⊢ (<g,i=j(rho)> o cube+(J;j) K <alpha, x1>) = (<rho> o cube+(I;i) o <g>+ K <alpha, x1>) ∈ Gamma(K)

---

Latex:

---

Latex:

1.  Gamma  :  CubicalSet\{j\}
2.  I  :  fset(\mBbbN{})
3.  J  :  fset(\mBbbN{})
4.  i  :  \{i:\mBbbN{}|  \mneg{}i  \mmember{}  I\} 
5.  j  :  \{j:\mBbbN{}|  \mneg{}j  \mmember{}  J\} 
6.  g  :  J  {}\mrightarrow{}  I
7.  rho  :  Gamma(I+i)
8.  \mforall{}[A,B:j\mvdash{}].  \mforall{}[f:A  j{}\mrightarrow{}  B].  \mforall{}[g:I:fset(\mBbbN{})  {}\mrightarrow{}  A(I)  {}\mrightarrow{}  B(I)].    f  =  g  supposing  f  =  g
9.  K  :  fset(\mBbbN{})
10.  x  :  formal-cube(J).\mBbbI{}(K)
\mvdash{}  (<g,i=j(rho)>  o  cube+(J;j)  K  x)  =  (<rho>  o  cube+(I;i)  o  <g>+  K  x)


By

---

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

---

Home Index