---

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

.....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})
BY
{ EqualityIsType1 }

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

3
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}
⊢ a ∈ {Y, phi ⊢ _:A}

---

Latex:

---

Latex:
.....wf..... 
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\}
9.  x  :  \{X  \mvdash{}  \_:A\}
10.  t  =  x
11.  a  :  \{Y  \mvdash{}  \_:A\}
\mvdash{}  istype(t  =  a)


By

---

Latex:
EqualityIsType1

---

Home Index