---

Step * of Lemma context-map_wf

No Annotations
∀I:fset(ℕ). ∀Gamma:j⊢. ∀rho:Gamma(I).  (<rho> ∈ formal-cube(I) j⟶ Gamma)
BY
{ PresheafMLTTInstance Obid: ps-context-map_wf⋅ }

---

Latex:

---

Latex:
No  Annotations
\mforall{}I:fset(\mBbbN{}).  \mforall{}Gamma:j\mvdash{}.  \mforall{}rho:Gamma(I).    (<rho>  \mmember{}  formal-cube(I)  j{}\mrightarrow{}  Gamma)


By

---

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

---

Home Index