---

Step * of Lemma cubical-type-cumulativity2

No Annotations
∀[X:j⊢]. ({X ⊢ _} ⊆r cubical-type{[j | i]:l}(X))
BY
{ PresheafMLTTInstance Obid: presheaf-type-cumulativity2⋅ }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:j\mvdash{}].  (\{X  \mvdash{}  \_\}  \msubseteq{}r  cubical-type\{[j  |  i]:l\}(X))


By

---

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

---

Home Index