---

Step * 1 1 1 1 2 2 2 2 1 1 of Lemma presw-pres-c1


1. G : CubicalSet{j}
2. phi : {G ⊢ _:𝔽}
3. A : {G.𝕀 ⊢ _}
4. v : {G.𝕀 ⊢ _:A}
⊢ v = ((v)p+)[0(𝕀)]+ ∈ {G, phi.𝕀 ⊢ _:A}
BY
{ Assert ⌜{G.𝕀 ⊢ _:A} ⊆r {G, phi.𝕀 ⊢ _:A}⌝⋅ }

1
.....assertion..... 
1. G : CubicalSet{j}
2. phi : {G ⊢ _:𝔽}
3. A : {G.𝕀 ⊢ _}
4. v : {G.𝕀 ⊢ _:A}
⊢ {G.𝕀 ⊢ _:A} ⊆r {G, phi.𝕀 ⊢ _:A}

2
1. G : CubicalSet{j}
2. phi : {G ⊢ _:𝔽}
3. A : {G.𝕀 ⊢ _}
4. v : {G.𝕀 ⊢ _:A}
5. {G.𝕀 ⊢ _:A} ⊆r {G, phi.𝕀 ⊢ _:A}
⊢ v = ((v)p+)[0(𝕀)]+ ∈ {G, phi.𝕀 ⊢ _:A}

---

Latex:

---

Latex:

1.  G  :  CubicalSet\{j\}
2.  phi  :  \{G  \mvdash{}  \_:\mBbbF{}\}
3.  A  :  \{G.\mBbbI{}  \mvdash{}  \_\}
4.  v  :  \{G.\mBbbI{}  \mvdash{}  \_:A\}
\mvdash{}  v  =  ((v)p+)[0(\mBbbI{})]+


By

---

Latex:
Assert  \mkleeneopen{}\{G.\mBbbI{}  \mvdash{}  \_:A\}  \msubseteq{}r  \{G,  phi.\mBbbI{}  \mvdash{}  \_:A\}\mkleeneclose{}\mcdot{}

---

Home Index