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