Step
*
of Lemma
cubical-apply_wf
No Annotations
∀[X:j⊢]. ∀[A:{X ⊢ _}]. ∀[B:{X.A ⊢ _}]. ∀[w:{X ⊢ _:ΠA B}]. ∀[u:{X ⊢ _:A}]. (cubical-apply(w;u) ∈ {X ⊢ _:(B)[u]})
BY
{ PresheafMLTTInstance Obid: presheaf-apply_wf⋅ }
Latex:
Latex:
No Annotations
\mforall{}[X:j\mvdash{}]. \mforall{}[A:\{X \mvdash{} \_\}]. \mforall{}[B:\{X.A \mvdash{} \_\}]. \mforall{}[w:\{X \mvdash{} \_:\mPi{}A B\}]. \mforall{}[u:\{X \mvdash{} \_:A\}].
(cubical-apply(w;u) \mmember{} \{X \mvdash{} \_:(B)[u]\})
By
Latex:
PresheafMLTTInstance Obid: presheaf-apply\_wf\mcdot{}
Home
Index