---

Step * of Lemma cubical-type-cumulativity

No Annotations
∀[X:j⊢]. ({X ⊢ _} ⊆r {X ⊢' _})
BY
{ PresheafMLTTInstance Obid: presheaf-type-cumulativity⋅ }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:j\mvdash{}].  (\{X  \mvdash{}  \_\}  \msubseteq{}r  \{X  \mvdash{}'  \_\})


By

---

Latex:
PresheafMLTTInstance  Obid:  presheaf-type-cumulativity\mcdot{}

---

Home Index