---

Step * of Lemma subset-cubical-term2

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

---

Latex:

---

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


By

---

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

---

Home Index