---

Step * 1 1 of Lemma subset-iota-is-id

.....wf..... 
1. H : CubicalSet{j}
2. phi : {H ⊢ _:𝔽}
3. v : {H, phi ⊢ _}
⊢ H, phi j⊢
BY
{ Auto }

---

Latex:

---

Latex:
.....wf..... 
1.  H  :  CubicalSet\{j\}
2.  phi  :  \{H  \mvdash{}  \_:\mBbbF{}\}
3.  v  :  \{H,  phi  \mvdash{}  \_\}
\mvdash{}  H,  phi  j\mvdash{}


By

---

Latex:
Auto

---

Home Index