---

Step * of Lemma context-map-comp2

No Annotations
∀[G:j⊢]. ∀[I,J:fset(ℕ)]. ∀[f:J ⟶ I]. ∀[a:G(I)].  (<a> o <f> = <f(a)> ∈ formal-cube(J) ij⟶ G)
BY
{ PresheafMLTTInstance Obid: ps-context-map-comp2⋅ }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[G:j\mvdash{}].  \mforall{}[I,J:fset(\mBbbN{})].  \mforall{}[f:J  {}\mrightarrow{}  I].  \mforall{}[a:G(I)].    (<a>  o  <f>  =  <f(a)>)


By

---

Latex:
PresheafMLTTInstance  Obid:  ps-context-map-comp2\mcdot{}

---

Home Index