---

Step * of Lemma csm-comp-context-map

No Annotations
∀[Gamma,Delta:j⊢]. ∀[sigma:Delta j⟶ Gamma]. ∀[I:fset(ℕ)]. ∀[rho:Delta(I)].
  (sigma o <rho> = <(sigma)rho> ∈ formal-cube(I) j⟶ Gamma)
BY
{ (InstLemma_o (ioid Obid: pscm-comp-context-map) [⌜parm{j}⌝;⌜parm{j}⌝;⌜CubeCat⌝]⋅ THENA Auto) }

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

---

Latex:

---

Latex:
No  Annotations
\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:
(InstLemma\_o  (ioid  Obid:  pscm-comp-context-map)  [\mkleeneopen{}parm\{j\}\mkleeneclose{};\mkleeneopen{}parm\{j\}\mkleeneclose{};\mkleeneopen{}CubeCat\mkleeneclose{}]\mcdot{}  THENA  Auto)

---

Home Index