---

Step * of Lemma subset-cubical-term

No Annotations
∀[X,Y:j⊢].  ∀[A:{X ⊢ _}]. ({X ⊢ _:A} ⊆r {Y ⊢ _:A}) supposing sub_cubical_set{j:l}(Y; X)
BY
{ PresheafMLTTInstance Obid: subset-presheaf-term⋅ }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X,Y:j\mvdash{}].    \mforall{}[A:\{X  \mvdash{}  \_\}].  (\{X  \mvdash{}  \_:A\}  \msubseteq{}r  \{Y  \mvdash{}  \_:A\})  supposing  sub\_cubical\_set\{j:l\}(Y;  X)


By

---

Latex:
PresheafMLTTInstance  Obid:  subset-presheaf-term\mcdot{}

---

Home Index