---

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


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]}
BY
{ ((D 0 THENA Auto) THEN D -1 THEN MemTypeCD) }

1
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}
9. x : {X ⊢ _:A}
10. t = x ∈ {X, phi ⊢ _:A}
⊢ x ∈ {Y ⊢ _:A}

2
.....set predicate..... 
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}
9. x : {X ⊢ _:A}
10. t = x ∈ {X, phi ⊢ _:A}
⊢ t = x ∈ {Y, phi ⊢ _:A}

3
.....wf..... 
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}
9. x : {X ⊢ _:A}
10. t = x ∈ {X, phi ⊢ _:A}
11. a : {Y ⊢ _:A}
⊢ istype(t = a ∈ {Y, phi ⊢ _:A})

---

Latex:

---

Latex:

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\}
8.  \{X,  phi  \mvdash{}  \_:A\}  \msubseteq{}r  \{Y,  phi  \mvdash{}  \_:A\}
\mvdash{}  \{X  \mvdash{}  \_:A[phi  |{}\mrightarrow{}  t]\}  \msubseteq{}r  \{Y  \mvdash{}  \_:A[phi  |{}\mrightarrow{}  t]\}


By

---

Latex:
((D  0  THENA  Auto)  THEN  D  -1  THEN  MemTypeCD)

---

Home Index