---

Step * of Lemma subset-constrained-cubical-term

No Annotations
∀[X,Y:j⊢].
  ∀[A:{X ⊢ _}]. ∀[phi:{X ⊢ _:𝔽}]. ∀[t:{X, phi ⊢ _:A}].  ({X ⊢ _:A[phi |⟶ t]} ⊆r {Y ⊢ _:A[phi |⟶ t]}) 
  supposing sub_cubical_set{j:l}(Y; X)
BY
{ (InstLemma `subset-cubical-term` []
   THEN RepeatFor 4 (ParallelLast')
   THEN Auto
   THEN Assert ⌜{X, phi ⊢ _:A} ⊆r {Y, phi ⊢ _:A}⌝⋅) }

1
.....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}

2
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}
8. {X, phi ⊢ _:A} ⊆r {Y, phi ⊢ _:A}
⊢ {X ⊢ _:A[phi |⟶ t]} ⊆r {Y ⊢ _:A[phi |⟶ t]}

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X,Y:j\mvdash{}].
    \mforall{}[A:\{X  \mvdash{}  \_\}].  \mforall{}[phi:\{X  \mvdash{}  \_:\mBbbF{}\}].  \mforall{}[t:\{X,  phi  \mvdash{}  \_:A\}].
        (\{X  \mvdash{}  \_:A[phi  |{}\mrightarrow{}  t]\}  \msubseteq{}r  \{Y  \mvdash{}  \_:A[phi  |{}\mrightarrow{}  t]\}) 
    supposing  sub\_cubical\_set\{j:l\}(Y;  X)


By

---

Latex:
(InstLemma  `subset-cubical-term`  []
  THEN  RepeatFor  4  (ParallelLast')
  THEN  Auto
  THEN  Assert  \mkleeneopen{}\{X,  phi  \mvdash{}  \_:A\}  \msubseteq{}r  \{Y,  phi  \mvdash{}  \_:A\}\mkleeneclose{}\mcdot{})

---

Home Index