---

Step * 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))
⊢ <g,i=j(rho)> o cube+(J;j) = <rho> o cube+(I;i) o <g>+ ∈ (I:fset(ℕ) ⟶ formal-cube(J).𝕀(I) ⟶ Gamma(I))
BY
{ ((FunExt THENA Auto) THEN RenameVar `K' (-1) THEN (FunExt THENA Auto)) }

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. 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)

---

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
\mvdash{}  <g,i=j(rho)>  o  cube+(J;j)  =  <rho>  o  cube+(I;i)  o  <g>+


By

---

Latex:
((FunExt  THENA  Auto)  THEN  RenameVar  `K'  (-1)  THEN  (FunExt  THENA  Auto))

---

Home Index