---

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


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)
BY
{ (RepeatFor 5 (ParallelLast) THEN NthHypSq (-1) THEN RepeatFor 2 ((Computation THEN EqCD THEN Try (Trivial)))) }

---

Latex:

---

Latex:

1.  \mforall{}[Gamma,Delta:j\mvdash{}].  \mforall{}[sigma:Delta  j{}\mrightarrow{}  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:
(RepeatFor  5  (ParallelLast)
  THEN  NthHypSq  (-1)
  THEN  RepeatFor  2  ((Computation  THEN  EqCD  THEN  Try  (Trivial))))

---

Home Index