---

Step * of Lemma cs-predicate_wf

No Annotations
∀[X:j⊢]. ∀[P:I:fset(ℕ) ⟶ X(I) ⟶ ℙ{[i | j']}].  (cs-predicate(X;I,rho.P[I;rho]) ∈ ℙ{[i | j']})
BY
{ PresheafMLTTInstance Obid: psc-predicate_wf⋅ }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:j\mvdash{}].  \mforall{}[P:I:fset(\mBbbN{})  {}\mrightarrow{}  X(I)  {}\mrightarrow{}  \mBbbP{}\{[i  |  j']\}].    (cs-predicate(X;I,rho.P[I;rho])  \mmember{}  \mBbbP{}\{[i  |  j']\})


By

---

Latex:
PresheafMLTTInstance  Obid:  psc-predicate\_wf\mcdot{}

---

Home Index