---

Step * of Lemma context-map-ap-type

No Annotations
∀[I:fset(ℕ)]. ∀[Gamma:j⊢]. ∀[rho:Gamma(I)]. ∀[A:{Gamma ⊢ _}].  formal-cube(I) ⊢ (A)<rho>
BY
{ PresheafMLTTInstance Obid: ps-context-map-ap-type⋅ }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[I:fset(\mBbbN{})].  \mforall{}[Gamma:j\mvdash{}].  \mforall{}[rho:Gamma(I)].  \mforall{}[A:\{Gamma  \mvdash{}  \_\}].    formal-cube(I)  \mvdash{}  (A)<rho>


By

---

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

---

Home Index