---

Step * of Lemma csm-subset-domain

No Annotations
∀[X,Y,Z:j⊢].  Y j⟶ X ⊆r Z j⟶ X supposing sub_cubical_set{j:l}(Z; Y)
BY
{ PresheafMLTTInstance Obid: pscm-subset-domain⋅ }

---

Latex:

---

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


By

---

Latex:
PresheafMLTTInstance  Obid:  pscm-subset-domain\mcdot{}

---

Home Index