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