---

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

No Annotations
∀[Gamma:j⊢]. ∀[I,J:fset(ℕ)]. ∀[i:{i:ℕ| ¬i ∈ I} ]. ∀[j:{j:ℕ| ¬j ∈ J} ]. ∀[g:J ⟶ I]. ∀[rho:Gamma(I+i)].
  (<g,i=j(rho)> o cube+(J;j) = <rho> o cube+(I;i) o <g>+ ∈ formal-cube(J).𝕀 j⟶ Gamma)
BY
{ (Intros THEN (CsmEqual THENW 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))
⊢ <g,i=j(rho)> o cube+(J;j) = <rho> o cube+(I;i) o <g>+ ∈ (I:fset(ℕ) ⟶ formal-cube(J).𝕀(I) ⟶ Gamma(I))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[Gamma:j\mvdash{}].  \mforall{}[I,J:fset(\mBbbN{})].  \mforall{}[i:\{i:\mBbbN{}|  \mneg{}i  \mmember{}  I\}  ].  \mforall{}[j:\{j:\mBbbN{}|  \mneg{}j  \mmember{}  J\}  ].  \mforall{}[g:J  {}\mrightarrow{}  I].  \mforall{}[rho:Gamma(I+i)\000C].
    (<g,i=j(rho)>  o  cube+(J;j)  =  <rho>  o  cube+(I;i)  o  <g>+)


By

---

Latex:
(Intros  THEN  (CsmEqual  THENW  Auto))

---

Home Index