Step
*
of Lemma
csm-dependent_wf
No Annotations
∀X,Delta:j⊢. ∀A:{X ⊢ _}. ∀s:Delta j⟶ X.  ((s)dep ∈ Delta.(A)s j⟶ X.A)
BY
{ PresheafMLTTInstance Obid: pscm-dependent_wf⋅ }
Latex:
Latex:
No  Annotations
\mforall{}X,Delta:j\mvdash{}.  \mforall{}A:\{X  \mvdash{}  \_\}.  \mforall{}s:Delta  j{}\mrightarrow{}  X.    ((s)dep  \mmember{}  Delta.(A)s  j{}\mrightarrow{}  X.A)
By
Latex:
PresheafMLTTInstance  Obid:  pscm-dependent\_wf\mcdot{}
Home
Index