---

Step * 1 of Lemma csm-comp-context-map


1. ∀[Gamma,Delta:ps_context{j:l}(CubeCat)]. ∀[sigma:psc_map{j:l}(CubeCat; Delta; Gamma)]. ∀[I:cat-ob(CubeCat)].
   ∀[rho:Delta(I)].
     (sigma o <rho> = <(sigma)rho> ∈ psc_map{[j | j]:l}(CubeCat; Yoneda(I); Gamma))
⊢ ∀[Gamma,Delta:j⊢]. ∀[sigma:Delta j⟶ Gamma]. ∀[I:fset(ℕ)]. ∀[rho:Delta(I)].
    (sigma o <rho> = <(sigma)rho> ∈ formal-cube(I) j⟶ Gamma)
BY
{ Folds  ``cubical_set cube_set_map I_cube csm-comp context-map csm-ap`` (-1) }

1
1. ∀[Gamma,Delta:j⊢]. ∀[sigma:Delta j⟶ Gamma]. ∀[I:cat-ob(CubeCat)]. ∀[rho:Delta(I)].
     (sigma o <rho> = <(sigma)rho> ∈ Yoneda(I) j⟶ Gamma)
⊢ ∀[Gamma,Delta:j⊢]. ∀[sigma:Delta j⟶ Gamma]. ∀[I:fset(ℕ)]. ∀[rho:Delta(I)].
    (sigma o <rho> = <(sigma)rho> ∈ formal-cube(I) j⟶ Gamma)

---

Latex:

---

Latex:

1.  \mforall{}[Gamma,Delta:ps\_context\{j:l\}(CubeCat)].  \mforall{}[sigma:psc\_map\{j:l\}(CubeCat;  Delta;  Gamma)].
      \mforall{}[I:cat-ob(CubeCat)].  \mforall{}[rho:Delta(I)].
          (sigma  o  <rho>  =  <(sigma)rho>)
\mvdash{}  \mforall{}[Gamma,Delta:j\mvdash{}].  \mforall{}[sigma:Delta  j{}\mrightarrow{}  Gamma].  \mforall{}[I:fset(\mBbbN{})].  \mforall{}[rho:Delta(I)].
        (sigma  o  <rho>  =  <(sigma)rho>)


By

---

Latex:
Folds    ``cubical\_set  cube\_set\_map  I\_cube  csm-comp  context-map  csm-ap``  (-1)

---

Home Index