Step
*
of Lemma
sub-cubical-set_wf
No Annotations
∀[X:j⊢]. ∀[P:I:fset(ℕ) ⟶ X(I) ⟶ ℙ{j'}].  X | 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