---

Step * of Lemma csm-subset-subtype

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

---

Latex:

---

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


By

---

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

---

Home Index