---

Step * 1 of Lemma subset-constrained-cubical-term

.....assertion..... 
1. X : CubicalSet{j}
2. Y : CubicalSet{j}
3. sub_cubical_set{j:l}(Y; X)
4. A : {X ⊢ _}
5. {X ⊢ _:A} ⊆r {Y ⊢ _:A}
6. phi : {X ⊢ _:𝔽}
7. t : {X, phi ⊢ _:A}
⊢ {X, phi ⊢ _:A} ⊆r {Y, phi ⊢ _:A}
BY
{ Auto }

---

Latex:

---

Latex:
.....assertion..... 
1.  X  :  CubicalSet\{j\}
2.  Y  :  CubicalSet\{j\}
3.  sub\_cubical\_set\{j:l\}(Y;  X)
4.  A  :  \{X  \mvdash{}  \_\}
5.  \{X  \mvdash{}  \_:A\}  \msubseteq{}r  \{Y  \mvdash{}  \_:A\}
6.  phi  :  \{X  \mvdash{}  \_:\mBbbF{}\}
7.  t  :  \{X,  phi  \mvdash{}  \_:A\}
\mvdash{}  \{X,  phi  \mvdash{}  \_:A\}  \msubseteq{}r  \{Y,  phi  \mvdash{}  \_:A\}


By

---

Latex:
Auto

---

Home Index