---

Step * of Lemma cubical-type-restriction_wf

No Annotations
∀[X:j⊢]. ∀[T:{X ⊢ _}]. ∀[psi:I:fset(ℕ) ⟶ alpha:X(I) ⟶ T(alpha) ⟶ ℙ{[i' | j']}].
  (cubical-type-restriction(X;T;I,a,t.psi[I;a;t]) ∈ ℙ{[i' | j']})
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:j\mvdash{}].  \mforall{}[T:\{X  \mvdash{}  \_\}].  \mforall{}[psi:I:fset(\mBbbN{})  {}\mrightarrow{}  alpha:X(I)  {}\mrightarrow{}  T(alpha)  {}\mrightarrow{}  \mBbbP{}\{[i'  |  j']\}].
    (cubical-type-restriction(X;T;I,a,t.psi[I;a;t])  \mmember{}  \mBbbP{}\{[i'  |  j']\})


By

---

Latex:
ProveWfLemma

---

Home Index