---

Step * of Lemma istype-cubical-type-at

No Annotations
∀[X:j⊢]. ∀[I:fset(ℕ)]. ∀[a:X(I)]. ∀[A:{X ⊢ _}].  istype(A(a))
BY
{ Auto }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:j\mvdash{}].  \mforall{}[I:fset(\mBbbN{})].  \mforall{}[a:X(I)].  \mforall{}[A:\{X  \mvdash{}  \_\}].    istype(A(a))


By

---

Latex:
Auto

---

Home Index