Step * of Lemma sub-cubical-set_wf

No Annotations
[X:j⊢]. ∀[P:I:fset(ℕ) ⟶ X(I) ⟶ ℙ{j'}].  I,rho.P[I;rho] j⊢ supposing cs-predicate(X;I,rho.P[I;rho])
BY
PresheafMLTTInstance Obid: sub-presheaf-set_wf⋅ }


Latex:


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


By


Latex:
PresheafMLTTInstance  Obid:  sub-presheaf-set\_wf\mcdot{}




Home Index